proposition: Lemma MZ_det_A n : MZ_det (A n) = 1.
proof: Proof. Proof using Hb_nat. rewrite <- MZ_expo_A. rewrite Det22_expo with (Rminus := Z.sub); auto. rewrite MZ_det_B. rewrite mscal_of_unit; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)