proposition: Lemma comm: forall (R:Type)`{Ring R}(c : Z) (x : R), x * (gen_phiZ c) == (gen_phiZ c) * x.
proof: Proof. induction c. - intros. simpl. gen_rewrite. - simpl. intros. rewrite <- same_gen. induction p. + simpl. gen_rewrite. rewrite IHp. reflexivity. + simpl. gen_rewrite. rewrite IHp. reflexivity. + simpl. gen_rewrite. - simpl. intros. rewrite <- same_gen. induction p. + simpl. generalize IHp. clear IHp. gen_rewrite. intro IHp. rewrite IHp. reflexivity. + simpl. generalize IHp. clear IHp. gen_rewrite. intro IHp. rewrite IHp. reflexivity. + simpl. gen_rewrite. Qed.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool ZArith Algebra_syntax Ncring Ncring_polynom Ncring_initial