proposition: Corollary Pell_alpha_nat' b x y : 2 <= b -> x*x+y*y = 1+b*(x*y) -> { n | x = alpha_nat b n }.
proof: Proof. intros H1 H2. destruct (le_lt_dec y x) as [ H3 | H3 ]. + destruct Pell_alpha_nat with (3 := H2) as (n & ? & ?); auto. exists (S n); auto. + rewrite Nat.add_comm, (Nat.mul_comm x y) in H2. destruct Pell_alpha_nat with (3 := H2) as (n & ? & ?); auto; try lia. 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)