proposition: Theorem Pell_not_diag x : ~ Pell x x.
proof: Proof. Proof using Hb_nat. unfold Pell. intros H. assert (x*((2-b)*x) = 1) as H1. { rewrite <- H; ring. } generalize H1; intros H2. apply Z.eq_mul_1 in H1. destruct H1; subst; lia. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)