proposition: Lemma cring_catamorphism_fun_pos_mult {R} x y : cring_catamorphism_fun R (pos x * pos y)%int = cring_catamorphism_fun R (pos x) * cring_catamorphism_fun R (pos y).
proof: Proof. revert y. induction x as [|x IHx] using pos_peano_ind; intro y. { symmetry. apply left_identity. } change (cring_catamorphism_fun R (pos (pos_succ x * y)%pos) = cring_catamorphism_fun R (pos (pos_succ x)) * cring_catamorphism_fun R (pos y)). rewrite pos_mul_succ_l. refine (issemigrouppreserving_cring_catamorphism_fun_plus R (pos (x * y)%pos) (pos y) @ _). rewrite IHx. transitivity ((1 + cring_catamorphism_fun R (pos x)) * cring_catamorphism_fun R (pos y)). 2: simpl; by rewrite pos_peano_rec_beta_pos_succ. rewrite rng_dist_r. rewrite rng_mult_one_l. apply commutativity. Qed.
imports: Classes.interfaces.abstract_algebra Algebra.AbGroups Algebra.Rings.CRing Spaces.Int Spaces.Pos WildCat.Core