• Guillaume Melquiond's avatar
    Started a realization of real.real. · 72b12557
    Guillaume Melquiond authored
    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.
Real.v 5.43 KB