a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
⊢ Rat.blt (mk' nb db) (mk' na da) = false ↔ Rat.Nonneg (mk' nb db - mk' na da)
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
⊢ mk' na da ≤ mk' nb db ↔ Rat.Nonneg (mk' nb db - mk' na da)
change Rat.blt _ _ = false ↔ _
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
⊢ (if (decide ((mk' nb db).num < 0) && decide (0 ≤ (mk' na da).num)) = true then true
      else
        if (mk' nb db).num = 0 then decide (0 < (mk' na da).num)
        else
          if (decide (0 < (mk' nb db).num) && decide ((mk' na da).num ≤ 0)) = true then false
          else decide ((mk' nb db).num * ↑(mk' na da).den < (mk' na da).num * ↑(mk' nb db).den)) =
      false ↔
    Rat.Nonneg (mk' nb db - mk' na da)
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
⊢ Rat.blt (mk' nb db) (mk' na da) = false ↔ Rat.Nonneg (mk' nb db - mk' na da)
unfold Rat.blt
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
⊢ (if nb < 0 ∧ 0 ≤ na then False else if nb = 0 then na ≤ 0 else (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da) ↔
    Rat.Nonneg (mk' nb db - mk' na da)
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
⊢ (if (decide ((mk' nb db).num < 0) && decide (0 ≤ (mk' na da).num)) = true then true
      else
        if (mk' nb db).num = 0 then decide (0 < (mk' na da).num)
        else
          if (decide (0 < (mk' nb db).num) && decide ((mk' na da).num ≤ 0)) = true then false
          else decide ((mk' nb db).num * ↑(mk' na da).den < (mk' na da).num * ↑(mk' nb db).den)) =
      false ↔
    Rat.Nonneg (mk' nb db - mk' na da)
simp [-divInt_ofNat, mkRat_eq]
case inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ False ↔ Rat.Nonneg (mk' nb db - mk' na da)

case inr.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : nb = 0
⊢ na ≤ 0 ↔ Rat.Nonneg (mk' nb db - mk' na da)

case inr.inr
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
⊢ (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da ↔ Rat.Nonneg (mk' nb db - mk' na da)
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
⊢ (if nb < 0 ∧ 0 ≤ na then False else if nb = 0 then na ≤ 0 else (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da) ↔
    Rat.Nonneg (mk' nb db - mk' na da)
split_ifs with h h'
case inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ False ↔
    Rat.Nonneg
      (normalize ((mk' nb db).num * ↑(mk' na da).den - (mk' na da).num * ↑(mk' nb db).den)
        ((mk' nb db).den * (mk' na da).den))
case inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ False ↔ Rat.Nonneg (mk' nb db - mk' na da)
rw [Rat.sub_def]
case inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ (normalize (nb * ↑da - na * ↑db) (db * da)).num < 0
case inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ False ↔
    Rat.Nonneg
      (normalize ((mk' nb db).num * ↑(mk' na da).den - (mk' na da).num * ↑(mk' nb db).den)
        ((mk' nb db).den * (mk' na da).den))
simp [Rat.Nonneg]
case inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da)) < 0
case inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ (normalize (nb * ↑da - na * ↑db) (db * da)).num < 0
simp [normalize_eq]
case inl.Ha
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ nb * ↑da - na * ↑db < 0

case inl.Hb
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 < ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
case inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da)) < 0
apply Int.ediv_neg'
case inl.Ha
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ nb * ↑da < na * ↑db
case inl.Ha
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ nb * ↑da - na * ↑db < 0
rw [sub_neg]
case inl.Ha.a
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ nb * ↑da < ?inl.Ha.b

case inl.Ha.a
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ ?inl.Ha.b ≤ na * ↑db

case inl.Ha.b
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ ℤ
case inl.Ha
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ nb * ↑da < na * ↑db
apply lt_of_lt_of_le
case inl.Ha.a
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 < ↑da
case inl.Ha.a
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ nb * ↑da < ?inl.Ha.b
apply mul_neg_of_neg_of_pos h.1
no goals
case inl.Ha.a
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 < ↑da
rwa [Nat.cast_pos, pos_iff_ne_zero]
no goals
case inl.Ha.a
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 ≤ na * ↑db
apply mul_nonneg h.2 (Nat.cast_nonneg _)
case inl.Hb
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 < Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da)
case inl.Hb
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 < ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
simp only [Nat.cast_pos]
case inl.Hb.npos
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 < db * da
case inl.Hb
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 < Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da)
apply Nat.gcd_pos_of_pos_right
no goals
case inl.Hb.npos
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : nb < 0 ∧ 0 ≤ na
⊢ 0 < db * da
apply mul_pos <;> rwa [pos_iff_ne_zero]
case inr.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : nb = 0
⊢ na ≤ 0 ↔ Rat.Nonneg (mk' nb db - mk' na da)
case inr.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : nb = 0
⊢ na ≤ 0 ↔ Rat.Nonneg (mk' nb db - mk' na da)
simp only [divInt_ofNat, ←zero_iff_num_zero, mkRat_eq_zero hb] at h'
no goals
case inr.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : nb = 0
⊢ na ≤ 0 ↔ Rat.Nonneg (mk' nb db - mk' na da)
simp [h', Rat.Nonneg]
case inr.inr
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
⊢ (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da ↔
    0 ≤ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
case inr.inr
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
⊢ (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da ↔ Rat.Nonneg (mk' nb db - mk' na da)
simp [Rat.Nonneg, Rat.sub_def, normalize_eq]
case inr.inr.refine_1
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
⊢ 0 ≤ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))

case inr.inr.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : 0 ≤ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
x✝ : 0 < nb → 0 < na
⊢ na * ↑db ≤ nb * ↑da
case inr.inr
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
⊢ (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da ↔
    0 ≤ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
refine ⟨fun H => ?_, fun H _ => ?_⟩
case inr.inr.refine_1
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
⊢ 0 ≤ nb * ↑da - na * ↑db
case inr.inr.refine_1
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
⊢ 0 ≤ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
refine Int.ediv_nonneg ?_ (Nat.cast_nonneg _)
case inr.inr.refine_1
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
⊢ na * ↑db ≤ nb * ↑da
case inr.inr.refine_1
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
⊢ 0 ≤ nb * ↑da - na * ↑db
rw [sub_nonneg]
case inr.inr.refine_1
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
⊢ na * ↑db ≤ nb * ↑da
case inr.inr.refine_1
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
⊢ na * ↑db ≤ nb * ↑da
push_neg at h
case inr.inr.refine_1.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : nb < 0
⊢ na * ↑db ≤ nb * ↑da

case inr.inr.refine_1.inr
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : 0 < nb
⊢ na * ↑db ≤ nb * ↑da
case inr.inr.refine_1
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
⊢ na * ↑db ≤ nb * ↑da
obtain hb|hb := Ne.lt_or_lt h'
case inr.inr.refine_1.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : nb < 0
⊢ 0 < nb → 0 < na
case inr.inr.refine_1.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : nb < 0
⊢ na * ↑db ≤ nb * ↑da
apply H
case inr.inr.refine_1.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : nb < 0
H' : 0 < nb
⊢ 0 < na
case inr.inr.refine_1.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : nb < 0
⊢ 0 < nb → 0 < na
intro H'
no goals
case inr.inr.refine_1.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : nb < 0
H' : 0 < nb
⊢ 0 < na
exact (hb.trans H').false.elim
case inr.inr.refine_1.inr.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha✝ : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : 0 < nb
ha : na ≤ 0
⊢ na * ↑db ≤ nb * ↑da

case inr.inr.refine_1.inr.inr
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha✝ : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : 0 < nb
ha : 0 < na
⊢ na * ↑db ≤ nb * ↑da
case inr.inr.refine_1.inr
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : 0 < nb
⊢ na * ↑db ≤ nb * ↑da
obtain ha|ha := le_or_lt na 0
case inr.inr.refine_1.inr.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha✝ : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : 0 < nb
ha : na ≤ 0
⊢ 0 ≤ nb * ↑da
case inr.inr.refine_1.inr.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha✝ : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : 0 < nb
ha : na ≤ 0
⊢ na * ↑db ≤ nb * ↑da
apply le_trans <| mul_nonpos_of_nonpos_of_nonneg ha (Nat.cast_nonneg _)
no goals
case inr.inr.refine_1.inr.inl
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha✝ : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : 0 < nb
ha : na ≤ 0
⊢ 0 ≤ nb * ↑da
exact mul_nonneg hb.le (Nat.cast_nonneg _)
no goals
case inr.inr.refine_1.inr.inr
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha✝ : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb✝ : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h' : ¬nb = 0
H : (0 < nb → 0 < na) → na * ↑db ≤ nb * ↑da
h : nb < 0 → na < 0
hb : 0 < nb
ha : 0 < na
⊢ na * ↑db ≤ nb * ↑da
exact H (fun _ => ha)
case inr.inr.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : 0 ≤ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
x✝ : 0 < nb → 0 < na
⊢ 0 ≤ nb * ↑da - na * ↑db
case inr.inr.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : 0 ≤ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
x✝ : 0 < nb → 0 < na
⊢ na * ↑db ≤ nb * ↑da
rw [←sub_nonneg]
case inr.inr.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
x✝ : 0 < nb → 0 < na
H : nb * ↑da - na * ↑db < 0
⊢ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da)) < 0
case inr.inr.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
H : 0 ≤ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
x✝ : 0 < nb → 0 < na
⊢ 0 ≤ nb * ↑da - na * ↑db
contrapose! H
case inr.inr.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
x✝ : 0 < nb → 0 < na
H : nb * ↑da - na * ↑db < 0
⊢ 0 < ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
case inr.inr.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
x✝ : 0 < nb → 0 < na
H : nb * ↑da - na * ↑db < 0
⊢ (nb * ↑da - na * ↑db) / ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da)) < 0
apply Int.ediv_neg' H
case inr.inr.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
x✝ : 0 < nb → 0 < na
H : nb * ↑da - na * ↑db < 0
⊢ 0 < Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da)
case inr.inr.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
x✝ : 0 < nb → 0 < na
H : nb * ↑da - na * ↑db < 0
⊢ 0 < ↑(Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da))
simp only [Nat.cast_pos]
case inr.inr.refine_2.npos
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
x✝ : 0 < nb → 0 < na
H : nb * ↑da - na * ↑db < 0
⊢ 0 < db * da
case inr.inr.refine_2
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
x✝ : 0 < nb → 0 < na
H : nb * ↑da - na * ↑db < 0
⊢ 0 < Nat.gcd (Int.natAbs (nb * ↑da - na * ↑db)) (db * da)
apply Nat.gcd_pos_of_pos_right
no goals
case inr.inr.refine_2.npos
a✝ b✝ c a b : ℚ
na : ℤ
da : ℕ
ha : da ≠ 0
hared : Nat.coprime (Int.natAbs na) da
nb : ℤ
db : ℕ
hb : db ≠ 0
hbred : Nat.coprime (Int.natAbs nb) db
h : ¬(nb < 0 ∧ 0 ≤ na)
h' : ¬nb = 0
x✝ : 0 < nb → 0 < na
H : nb * ↑da - na * ↑db < 0
⊢ 0 < db * da
apply mul_pos <;> rwa [pos_iff_ne_zero]