proposition: Lemma sqrt_nonneg : forall a, 0<=√a.
proof: Proof. intros a. destruct (lt_ge_cases a 0) as [Ha|Ha]. - now rewrite (sqrt_neg _ Ha). - apply sqrt_spec_nonneg. destruct (sqrt_spec a Ha). order. Qed.
imports: NZAxioms NZMulOrder