proposition: Lemma nringS_ap_zero : forall m : nat, nring (R:=R) (S m) [#] [0].
proof: Proof. intros. apply pos_ap_zero. exact (pos_Snring m). Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)