proposition: Lemma nring_ap_zero_imp : forall n : nat, nring (R:=R) n [#] [0] -> 0 <> n.
proof: Proof. intros n H. induction n as [| n Hrecn]. simpl in H. elim (ap_irreflexive_unfolded _ _ H). apply O_S. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)