Theorem: Lean4Axiomatic.Rational.lt_substD_div_neg (Lean4Axiomatic/Rational/Order.lean)

State before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
⊢ p < q → q / r < p / r
Tactic:
intro (_ : p < q)
State after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
⊢ q / r < p / r

State before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
⊢ q / r < p / r
Tactic:
have : sgn (p - q) ≃ -1 := lt_sgn.mp ‹p < q›
State after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this : sgn (p - q) ≃ -1
⊢ q / r < p / r

State before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this : sgn (p - q) ≃ -1
⊢ q / r < p / r
Tactic:
have : sgn (q/r - p/r) ≃ sgn (p - q) := sgn_sub_cancelR_div_neg
State after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this✝ : sgn (p - q) ≃ -1
this : sgn (q / r - p / r) ≃ sgn (p - q)
⊢ q / r < p / r

State before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this✝ : sgn (p - q) ≃ -1
this : sgn (q / r - p / r) ≃ sgn (p - q)
⊢ q / r < p / r
Tactic:
have : sgn (q/r - p/r) ≃ -1 :=
  AA.eqv_substL (Rel.symm this) ‹sgn (p - q) ≃ -1›
State after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this✝¹ : sgn (p - q) ≃ -1
this✝ : sgn (q / r - p / r) ≃ sgn (p - q)
this : sgn (q / r - p / r) ≃ -1
⊢ q / r < p / r

State before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this✝¹ : sgn (p - q) ≃ -1
this✝ : sgn (q / r - p / r) ≃ sgn (p - q)
this : sgn (q / r - p / r) ≃ -1
⊢ q / r < p / r
Tactic:
have : q/r < p/r := lt_sgn.mpr this
State after:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this✝² : sgn (p - q) ≃ -1
this✝¹ : sgn (q / r - p / r) ≃ sgn (p - q)
this✝ : sgn (q / r - p / r) ≃ -1
this : q / r < p / r
⊢ q / r < p / r

State before:
ℕ ℤ ℚ : Type
inst✝¹¹ : Natural ℕ
inst✝¹⁰ : Integer ℤ
inst✝⁹ : Core ℚ
inst✝⁸ : Addition ℚ
inst✝⁷ : Multiplication ℚ
inst✝⁶ : Negation ℚ
inst✝⁵ : Sign ℚ
inst✝⁴ : Subtraction ℚ
inst✝³ : Reciprocation ℚ
inst✝² : Division ℚ
inst✝¹ : Order ℚ
p q r : ℚ
inst✝ : AP (sgn r ≃ -1)
x✝ : p < q
this✝² : sgn (p - q) ≃ -1
this✝¹ : sgn (q / r - p / r) ≃ sgn (p - q)
this✝ : sgn (q / r - p / r) ≃ -1
this : q / r < p / r
⊢ q / r < p / r
Tactic:
exact this
State after:
no goals