proposition: Lemma nring_ap_zero : forall n : nat, n <> 0 -> nring (R:=R) n [#] [0].
proof: Proof. intros n H. exact (nring_apart _ _ H). Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)