proposition: Lemma sqrt_up_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_up_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (sqrt_up_succ_le a Ha); order. Qed.
imports: NZAxioms NZMulOrder