proposition: Lemma pos_Snring : forall n : nat, ([0]:R) [<] Snring n.
proof: Proof. intro n. apply less_leEq_trans with ([1]:R). apply pos_one. stepl (nring (R:=R) 1). 2: simpl in |- *; algebra. unfold Snring in |- *. apply nring_leEq. auto with arith. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)