(n : nat) (x y : abgroup_Z) : ab_mul y (cyclic_in n x) = cyclic_in n (y * x)%int. Proof. lhs_V nrapply ab_mul_natural. apply ap, abgroup_Z_ab_mul. Defined.
Require Import Basics.Overture Basics.Tactics WildCat.Core AbelianGroup