k x y : Nat
Hk : 0 < k
⊢ ¬y ≤ x / k ↔ ¬y * k ≤ x
k x y : Nat
Hk : 0 < k
⊢ x / k < y ↔ x < y * k
rw [← Nat.not_le, ← Nat.not_le]
no goals
k x y : Nat
Hk : 0 < k
⊢ ¬y ≤ x / k ↔ ¬y * k ≤ x
exact not_congr (le_div_iff_mul_le Hk)