• 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
..
Abs.v Loading commit data...
MinMax.v Loading commit data...
Real.v Loading commit data...
Square.v Loading commit data...