• Guillaume Melquiond's avatar
    Add a realization of real.square. · 12daccee
    Guillaume Melquiond authored
    Remark about the theory: if one considers that the square root is always
    nonnegative (by definition in Coq), then Lemma Sqrt_positive has an
    extraneous hypothesis.
    12daccee
Name
Last commit
Last update
..
coq/real Loading commit data...