isNNRat_le_true — Mathlib

Lean4
theorem isNNRat_le_true [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] :
    {a b : α} →
      {na nb : ℕ} → {da db : ℕ} → IsNNRat a na da → IsNNRat b nb db → decide (Nat.mul na (db) ≤ Nat.mul nb (da)) → a ≤ b
  | _, _, _, _, da, db, ⟨_, rfl⟩, ⟨_, rfl⟩, h =>
    by
    have h := (Nat.cast_le (α := α)).mpr <| of_decide_eq_true h
    have ha : 0 ≤ ⅟(da : α) := invOf_nonneg.mpr <| Nat.cast_nonneg da
    have hb : 0 ≤ ⅟(db : α) := invOf_nonneg.mpr <| Nat.cast_nonneg db
    have h := (mul_le_mul_of_nonneg_left · hb) <| mul_le_mul_of_nonneg_right h ha
    rw [← mul_assoc, Nat.commute_cast] at h
    simp only [Nat.mul_eq, Nat.cast_mul, mul_invOf_cancel_right'] at h
    rwa [Nat.commute_cast] at h
Похожие утверждения