proposition: Lemma sqrt_up_nonneg : forall a, 0<=√°a.
proof: Proof. intros a. destruct (le_gt_cases a 0) as [Ha|Ha]. - now rewrite sqrt_up_eqn0. - rewrite sqrt_up_eqn; trivial. apply le_le_succ_r, sqrt_nonneg. Qed.
imports: NZAxioms NZMulOrder