Mentions légales du service

Skip to content
  • 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