proposition: Lemma nring_nonneg : forall n : nat, [0] [<=] nring (R:=R) n.
proof: Proof. intro; induction n as [| n Hrecn]. apply leEq_reflexive. apply leEq_transitive with (nring (R:=R) n); [ assumption | apply less_leEq; simpl in |- *; apply less_plusOne ]. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)