proposition: Lemma sqrt_up_le_mono : forall a b, a <= b -> √°a <= √°b.
proof: Proof. intros a b H. destruct (le_gt_cases a 0) as [Ha|Ha]. - rewrite (sqrt_up_eqn0 _ Ha). apply sqrt_up_nonneg. - rewrite 2 sqrt_up_eqn by order. rewrite <- succ_le_mono. apply sqrt_le_mono, succ_le_mono. rewrite 2 (lt_succ_pred 0); order. Qed.
imports: NZAxioms NZMulOrder