proposition: Lemma nring_fac_ap_zero : forall n : nat, nring (R:=R) (fact n) [#] [0].
proof: Proof. intro n; apply nring_ap_zero. cut (0 < fact n). lia. apply lt_O_fact. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)