proposition: Lemma sqrtrem_spec n : 0<=n -> let (s,r) := sqrtrem n in n = s*s + r /\ 0 <= r <= 2*s.
proof: Proof. destruct n as [|p|p]. - now repeat split. - generalize (Pos.sqrtrem_spec p). simpl. destruct 1; simpl; subst; now repeat split. - now destruct 1. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass