Proving factor is at least 2

Stream: new members

[Gareth Ma]

Hi, I am feeling slightly dumb for this question :joy: But I am trying to prove that if x >= 2 is a divisor of y, then y / x >= 2. I am struggling to make any progess. I tried using by_contradiction then splitting y / x = 0 and y / x = 1, then handling each case, but it gets quite complicated. Is there any simple / decently-short solution?

example {x y : ℕ} (h : x ∣ y) (hx₁ : 2 ≤ x) (hx₂ : x < y) : 2 ≤ y / x :=
begin
  sorry
end

[Thomas Browning]

  rwa [nat.succ_le_iff, nat.lt_div_iff_mul_lt h, mul_one],

[Thomas Browning]

Note that hx₁ is actually unnecessary.

[Gareth Ma]

Thanks a lot, I was struggling to get literals like "2" to work with the nat succ stuff :(