proposition: Lemma pring_aux_nring : forall p n, pring_aux p (nring n) [=] nring (Pmult_nat p n).
proof: Proof. simple induction p; simpl in |- *; intros. astepl (nring n[+]pring_aux p0 (nring (n + n))). Step_final (nring (R:=R) n[+]nring (R:=R) (Pmult_nat p0 (n + n))). Step_final (pring_aux p0 (nring (n + n))). algebra. 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)