proposition: Fact A_minus u v : (v <= u)%nat -> A (u-v)%nat = A u ⊠ iA v.
proof: Proof. Proof using Hb_nat. intros H. rewrite <- (MZ_expo_A u). replace u with (u-v+v)%nat at 2 by lia. rewrite mscal_plus; auto. do 2 rewrite MZ_expo_A. rewrite <- M22mul_assoc with (1 := Zring). rewrite A_iA. rewrite M22mult_one_r with (1 := Zring). trivial. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)