no goals
α : Type ?u.268
a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ 0 < delta
decide
no goals
α : Type ?u.268
a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ a ≤ delta * (delta * a)
simpa [mul_assoc] using Nat.mul_le_mul_right a (by decide : 1 ≤ delta * delta)
no goals
α : Type ?u.268
a b : ℕ
h₁ : delta * a < b
h₂ : delta * b < a
⊢ 1 ≤ delta * delta
decide