proposition: Lemma pos_nring_fac : forall n : nat, [0] [<] nring (R:=R) (fact n).
proof: Proof. intro. astepl (nring (R:=R) 0). apply nring_less. apply lt_O_fact. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)