proposition: Lemma sqrtrem_spec n : let (s,r) := sqrtrem n in n = s*s + r /\ r <= 2*s.
proof: Proof. destruct n as [|p]. - now split. - generalize (Pos.sqrtrem_spec p). simpl. destruct 1; simpl; subst; now split. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties