proposition: Fact M22scal_morph : forall k x, morph22 (M22scal mX k x) = M22scal mY 〚 k 〛 (morph22 x).
proof: Proof. Proof using Hphi. destruct Hphi as [ G1 G2 G3 G4 G6 ]. intros k (((?&?)&?)&?); apply M22_equal; auto. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)