proposition: Fact expo22_morph n x : morph22 (mscal (MU22 pX mX) (ID_22 zX oX) n x) = mscal (MU22 pY mY) (ID_22 zY oY) n (morph22 x).
proof: Proof. Proof using Hphi. destruct Hphi as [ G1 G2 G3 G4 G6 ]. induction n as [ | n IHn ]. + do 2 rewrite mscal_0; apply M22_equal; auto. + do 2 rewrite mscal_S. rewrite MU22_morph, IHn; auto. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)