proposition: Fact A_iA n : A n ⊠ iA n = MZ_one.
proof: Proof. Proof using Hb_nat. generalize (alpha_Pell n); unfold Pell; intros H. apply M22_equal; try ring; simpl; rewrite alpha_fix_3, <- H; ring. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)