proposition: Lemma sqrt_spec n : 0<=n -> let s := sqrt n in s*s <= n < (succ s)*(succ s).
proof: Proof. destruct n as [|p|p]. - now repeat split. - unfold sqrt. intros _. simpl succ. rewrite Pos.add_1_r. apply (Pos.sqrt_spec p). - now destruct 1. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass