-
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
Prochaines maintenances programmées: lundi 06/05, lundi 03/06, lundi 01/07
Pour plus d'informations: https://doc-si.inria.fr/display/SU/Gitlab
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.