Theorem: Imo1988P6.constant_descent_vieta_jumping
Proof state before:
case inr
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H y x
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
this :
  ∀ (x y : ℕ) {claim : Prop} {H : ℕ → ℕ → Prop},
    H x y →
      ∀ (B C : ℕ → ℤ) (base : ℕ → ℕ → Prop),
        (∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0) →
          (∀ {x y : ℕ}, H x y ↔ H y x) →
            (∀ {x : ℕ}, H x 0 → claim) →
              (∀ {x : ℕ}, H x x → claim) →
                (∀ {x y : ℕ},
                    0 < x →
                      x < y →
                        ¬base x y →
                          H x y →
                            ∀ (y' : ℤ),
                              y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x) →
                  (∀ {x y : ℕ}, H x y → base x y → claim) → x ≤ y → claim
hxy : ¬x ≤ y
⊢ claim
Tactic:
apply this y x h₀ B C base _ _ _ _ _ _ (le_of_not_le hxy)
Proof state after:
x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H y x
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
this :
  ∀ (x y : ℕ) {claim : Prop} {H : ℕ → ℕ → Prop},
    H x y →
      ∀ (B C : ℕ → ℤ) (base : ℕ → ℕ → Prop),
        (∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0) →
          (∀ {x y : ℕ}, H x y ↔ H y x) →
            (∀ {x : ℕ}, H x 0 → claim) →
              (∀ {x : ℕ}, H x x → claim) →
                (∀ {x y : ℕ},
                    0 < x →
                      x < y →
                        ¬base x y →
                          H x y →
                            ∀ (y' : ℤ),
                              y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x) →
                  (∀ {x y : ℕ}, H x y → base x y → claim) → x ≤ y → claim
hxy : ¬x ≤ y
⊢ ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0

x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H y x
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
this :
  ∀ (x y : ℕ) {claim : Prop} {H : ℕ → ℕ → Prop},
    H x y →
      ∀ (B C : ℕ → ℤ) (base : ℕ → ℕ → Prop),
        (∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0) →
          (∀ {x y : ℕ}, H x y ↔ H y x) →
            (∀ {x : ℕ}, H x 0 → claim) →
              (∀ {x : ℕ}, H x x → claim) →
                (∀ {x y : ℕ},
                    0 < x →
                      x < y →
                        ¬base x y →
                          H x y →
                            ∀ (y' : ℤ),
                              y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x) →
                  (∀ {x y : ℕ}, H x y → base x y → claim) → x ≤ y → claim
hxy : ¬x ≤ y
⊢ ∀ {x y : ℕ}, H x y ↔ H y x

x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H y x
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
this :
  ∀ (x y : ℕ) {claim : Prop} {H : ℕ → ℕ → Prop},
    H x y →
      ∀ (B C : ℕ → ℤ) (base : ℕ → ℕ → Prop),
        (∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0) →
          (∀ {x y : ℕ}, H x y ↔ H y x) →
            (∀ {x : ℕ}, H x 0 → claim) →
              (∀ {x : ℕ}, H x x → claim) →
                (∀ {x y : ℕ},
                    0 < x →
                      x < y →
                        ¬base x y →
                          H x y →
                            ∀ (y' : ℤ),
                              y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x) →
                  (∀ {x y : ℕ}, H x y → base x y → claim) → x ≤ y → claim
hxy : ¬x ≤ y
⊢ ∀ {x : ℕ}, H x 0 → claim

x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H y x
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
this :
  ∀ (x y : ℕ) {claim : Prop} {H : ℕ → ℕ → Prop},
    H x y →
      ∀ (B C : ℕ → ℤ) (base : ℕ → ℕ → Prop),
        (∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0) →
          (∀ {x y : ℕ}, H x y ↔ H y x) →
            (∀ {x : ℕ}, H x 0 → claim) →
              (∀ {x : ℕ}, H x x → claim) →
                (∀ {x y : ℕ},
                    0 < x →
                      x < y →
                        ¬base x y →
                          H x y →
                            ∀ (y' : ℤ),
                              y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x) →
                  (∀ {x y : ℕ}, H x y → base x y → claim) → x ≤ y → claim
hxy : ¬x ≤ y
⊢ ∀ {x : ℕ}, H x x → claim

x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H y x
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
this :
  ∀ (x y : ℕ) {claim : Prop} {H : ℕ → ℕ → Prop},
    H x y →
      ∀ (B C : ℕ → ℤ) (base : ℕ → ℕ → Prop),
        (∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0) →
          (∀ {x y : ℕ}, H x y ↔ H y x) →
            (∀ {x : ℕ}, H x 0 → claim) →
              (∀ {x : ℕ}, H x x → claim) →
                (∀ {x y : ℕ},
                    0 < x →
                      x < y →
                        ¬base x y →
                          H x y →
                            ∀ (y' : ℤ),
                              y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x) →
                  (∀ {x y : ℕ}, H x y → base x y → claim) → x ≤ y → claim
hxy : ¬x ≤ y
⊢ ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x

x y : ℕ
claim : Prop
H : ℕ → ℕ → Prop
h₀ : H y x
B C : ℕ → ℤ
base : ℕ → ℕ → Prop
H_quad : ∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0
H_symm : ∀ {x y : ℕ}, H x y ↔ H y x
H_zero : ∀ {x : ℕ}, H x 0 → claim
H_diag : ∀ {x : ℕ}, H x x → claim
H_desc :
  ∀ {x y : ℕ},
    0 < x →
      x < y →
        ¬base x y → H x y → ∀ (y' : ℤ), y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x
H_base : ∀ {x y : ℕ}, H x y → base x y → claim
this :
  ∀ (x y : ℕ) {claim : Prop} {H : ℕ → ℕ → Prop},
    H x y →
      ∀ (B C : ℕ → ℤ) (base : ℕ → ℕ → Prop),
        (∀ {x y : ℕ}, H x y ↔ ↑y * ↑y - B x * ↑y + C x = 0) →
          (∀ {x y : ℕ}, H x y ↔ H y x) →
            (∀ {x : ℕ}, H x 0 → claim) →
              (∀ {x : ℕ}, H x x → claim) →
                (∀ {x y : ℕ},
                    0 < x →
                      x < y →
                        ¬base x y →
                          H x y →
                            ∀ (y' : ℤ),
                              y' * y' - B x * y' + C x = 0 → y' = B x - ↑y → y' * ↑y = C x → 0 ≤ y' ∧ y' ≤ ↑x) →
                  (∀ {x y : ℕ}, H x y → base x y → claim) → x ≤ y → claim
hxy : ¬x ≤ y
⊢ ∀ {x y : ℕ}, H x y → base x y → claim