proposition: Theorem Pell_opposite_not x y : y < 0 -> 0 < x -> ~ Pell x y.
proof: Proof. Proof using Hb_nat. intros H1 H2 H3. red in H3. assert (0 <= - (b *x*y)) as H4. { replace (-(b*x*y)) with (b*x*-y) by ring. apply Z.mul_nonneg_nonneg; try lia. } assert (0 < x*x) as H5. { apply Z.mul_pos_pos; auto. } assert (0 < y*y) as H6. { apply Z.mul_neg_neg; auto. } revert H3 H4 H5 H6. generalize (x*x) (y*y) (b*x*y); intros; lia. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)