proposition: Fact expo22_scal k n U : expo22 n (M22scal k U) = M22scal (expoR n k) (expo22 n U).
proof: Proof. Proof using R_is_ring. induction n as [ | n IHn ]. + do 3 rewrite mscal_0; apply M22_equal; ring. + do 3 rewrite mscal_S. rewrite IHn. rewrite <- M22scal_MU22_l, <- M22scal_MU22_r. rewrite M22scal_mult; auto. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)