proposition: Lemma nring_different : forall R, Char0 R -> forall i j, i <> j -> nring i [#] (nring j:R).
proof: Proof. intros R H i j H0. elim (Cnat_total_order i j); intros. replace j with (i + (j - i)). astepr (nring i[+]nring (j - i):R). astepl (nring i[+][0]:R). apply op_lft_resp_ap. apply ap_symmetric_unfolded. apply H. lia. auto with arith. replace i with (j + (i - j)). astepl (nring j[+]nring (i - j):R). astepr (nring j[+] ([0]:R)). apply op_lft_resp_ap. apply H. lia. auto with arith. auto. Qed.
imports: CoRN.tactics.CornTac CoRN.algebra.CSums CoRN.algebra.CAbMonoids Coq.Sorting.Permutation CoRN.util.SetoidPermutation Coq.Setoids.Setoid Coq.Classes.Morphisms Coq(Lia)