proposition: Lemma nring_pos : forall m : nat, 0 < m -> [0] [<] nring (R:=R) m.
proof: Proof. intro m. elim m. intro; elim (Nat.lt_irrefl 0 H). clear m; intros. apply leEq_less_trans with (nring (R:=R) n). astepl (nring (R:=R) 0). apply nring_leEq; auto with arith. simpl in |- *; apply less_plusOne. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)