proposition: Fact Det22_expo n x : Det22 (expo22 n x) = expoR n (Det22 x).
proof: Proof. Proof using R_is_ring. induction n as [ | n IHn ]. + do 2 rewrite mscal_0; simpl; ring. + do 2 rewrite mscal_S. rewrite Det22_mult, IHn; ring. Qed.
imports: Arith ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime binomial sums)