proposition: Theorem Pell_zero_right x : Pell x 0 <-> x = 1 \/ x = -1.
proof: Proof. Proof using Hb_nat. rewrite Pell_sym; apply Pell_zero_left. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)