proposition: Lemma sqrt_succ_or : forall a, 0<=a -> √(S a) == S (√a) \/ √(S a) == √a.
proof: Proof. intros a Ha. destruct (le_gt_cases (√(S a)) (√a)) as [H|H]. - right. generalize (sqrt_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (sqrt_succ_le a Ha); order. Qed.
imports: NZAxioms NZMulOrder