proposition: Theorem Pell_zero_left y : Pell 0 y <-> y = 1 \/ y = -1.
proof: Proof. Proof using Hb_nat. unfold Pell; split. + intros H. assert ((y-1)*(y+1) = 0) as H1. { ring_simplify in H. ring_simplify; lia. } apply Zmult_integral in H1; lia. + intros [ | ]; subst; ring. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)