proposition: Theorem Pell_alpha_nat b x y : 2 <= b -> y <= x -> x*x+y*y = 1+b*(x*y) -> { n | x = alpha_nat b (S n) /\ y = alpha_nat b n }.
proof: Proof. intros Hb H2 H1. apply f_equal with (f := Z.of_nat) in H1. do 2 rewrite Nat2Z.inj_add in H1. do 4 rewrite Nat2Z.inj_mul in H1. simpl Z.of_nat in H1. apply Z.sub_move_r in H1. destruct (le_lt_dec x y) as [ H3 | H3 ]. + revert H1; replace y with x by lia; clear y H2 H3; intros H1. exfalso. apply (@Pell_not_diag _ Hb (Z.of_nat x)); red. rewrite <- H1; ring. + destruct (@Pell_alpha _ Hb (Z.of_nat x) (Z.of_nat y)) as (n & P1 & P2). * split. - apply Zle_0_nat. - apply inj_lt; trivial. * red; rewrite <- H1; ring. * unfold alpha_Z in P1, P2. apply Nat2Z.inj in P1. apply Nat2Z.inj in P2. exists n; auto. Qed.
imports: Arith Lia ZArith Undecidability.Shared.Libs.DLW.Utils(utils_tac gcd prime crt binomial sums) Undecidability.H10.ArithLibs(matrix Zp)