proposition: Lemma sqrt_spec n : 0<=n -> let s := sqrt n in s*s <= n < (succ s)*(succ s).
proof: Proof. intros _. destruct n as [|p]. - now split. - apply (Pos.sqrt_spec p). Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties