Theorem: Smt.Reconstruct.Int.ge_of_sub_eq (Smt/Reconstruct/Int/Lemmas.lean)

State before:
a b c d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
⊢ (a₁ ≥ a₂) = (b₁ ≥ b₂)
Tactic:
have {c x y : Int} (hc : c > 0) : (c * (x - y) ≥ 0) = (x - y ≥ 0) := by
  rw (config := { occs := .pos [1] }) [← Int.mul_zero c, ge_iff_le, Int.mul_le_mul_left hc]
State after:
a b c d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
this : ∀ {c x y : Int}, c > 0 → (c * (x - y) ≥ 0) = (x - y ≥ 0)
⊢ (a₁ ≥ a₂) = (b₁ ≥ b₂)

State before:
a b c d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
this : ∀ {c x y : Int}, c > 0 → (c * (x - y) ≥ 0) = (x - y ≥ 0)
⊢ (a₁ ≥ a₂) = (b₁ ≥ b₂)
Tactic:
rw [ge_eq_sub_ge_zero, @ge_eq_sub_ge_zero b₁, ← this hc₁, ← this hc₂, h]
State after:
no goals

State before:
a b c✝ d a₁ a₂ b₁ b₂ c₁ c₂ : Int
hc₁ : c₁ > 0
hc₂ : c₂ > 0
h : c₁ * (a₁ - a₂) = c₂ * (b₁ - b₂)
c x y : Int
hc : c > 0
⊢ (c * (x - y) ≥ 0) = (x - y ≥ 0)
Tactic:
rw (config := { occs := .pos [1] }) [← Int.mul_zero c, ge_iff_le, Int.mul_le_mul_left hc]
State after:
no goals