proposition: Theorem Pell_alpha x y : 0 <= y < x -> Pell x y -> { n | x = α (S (S n)) /\ y = α (S n) }.
proof: Proof. Proof using Hb_nat. induction on x y as IH with measure (Z.to_nat y); intros Hxy HP. destruct (Z.eq_dec y 0) as [ Hy | Hy ]. + exists 0%nat. rewrite alpha_fix_1, alpha_fix_2; split; auto. subst y; rewrite Pell_zero_right in HP; lia. + red in HP. assert (x*x = 1 + (b*y)*x - y*y) as H1. { rewrite <- HP; ring. } assert (0 < y*y) as H2. { apply Z.mul_pos_pos; lia. } assert (x <= (b*y)) as H3. { apply Zmult_le_reg_r with x; [ | rewrite H1 ]; lia. } assert (-(y*x) <= - (y*y)) as H4. { rewrite <- Z.opp_le_mono. nia. } assert (x > b*y-y) as H5. { apply Zmult_gt_reg_r with x; try lia. } destruct (IH y (b*y-x)) as (m & G1 & G2); try lia. - red; rewrite <- HP; ring. - exists (S m); split; auto. rewrite alpha_fix_3, <- G2, <- G1; ring. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)