This is just a proof of concept, since most definitions should just be
notations for the realization to be user-friendly. Moreover, the format of
the file will presumably evolve, if only for some information to properly
update it when the theories change.

Remark about the theory : Lemma mul_assoc_div has an extraneous hypothesis.
Indeed, as long as inverse is a total function, this lemma is an immediate
consequence of multiplication associativity.