proposition: Fact Pell_sym x y : Pell x y <-> Pell y x.
proof: Proof. unfold Pell; split; intros H; rewrite <- H; ring. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)