proposition: Lemma sqrtrem_sqrt n : fst (sqrtrem n) = sqrt n.
proof: Proof. destruct n as [|p]. - reflexivity. - unfold sqrtrem, sqrt, Pos.sqrt. destruct (Pos.sqrtrem p) as (s,r). now destruct r. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties