Effectively reasoning with Int and < in Core

Stream: Is there code for X?

[Siddharth Bhat]

Consider the MWE:

theorem foo {x y : Int} (hxLt : x < 2^(w - 1)) (hyLt : 0 ≤ y) : x / y < 2^(w - 1) := by
  have : y = 0 ∨ 0 < y := by omega
  rcases this with hy | hy
  · subst hy
    simp
    norm_cast
    apply Nat.pow_pos (by decide)
  · norm_cast
    apply Int.ediv_lt_of_lt_mul hy
    have : 0 < ((2 ^ (w - 1) : Nat) : Int) := by
      sorry
    apply Int.lt_of_lt_of_le hxLt
    sorry

This has two subgoals:

w : Nat
x y : Int
hxLt : x < 2 ^ (w - 1)
hyLt : 0 ≤ y
hy : 0 < y
⊢ 0 < ↑(2 ^ (w - 1))

and

case inr
w : Nat
x y : Int
hxLt : x < 2 ^ (w - 1)
hyLt : 0 ≤ y
hy : 0 < y
this : 0 < ↑(2 ^ (w - 1))
⊢ 2 ^ (w - 1) ≤ ↑(2 ^ (w - 1)) * y

where I'm stuck on, and I seem to lack the basic lemmata that I'd need to prove this. Ideally, I would dispatch the latter with a theorem that says that p < q * p when 0 < q, but I have no idea whether this theorem exists in Core and I'm being thick, or if I need to prove it!

[Robin Arnez]

You can do * 1 on the lhs, then use Int.mul_le_mul_of_nonneg:

theorem foo {x y : Int} (hxLt : x < 2^(w - 1)) (hyLt : 0 ≤ y) : x / y < 2^(w - 1) := by
  have : y = 0 ∨ 0 < y := by omega
  rcases this with hy | hy
  · subst hy
    simp
    norm_cast
    apply Nat.pow_pos (by decide)
  · apply Int.ediv_lt_of_lt_mul hy
    apply Int.lt_of_lt_of_le hxLt
    conv => lhs; apply (Int.mul_one _).symm
    refine Int.mul_le_mul_of_nonneg_left hy ?_
    norm_cast
    exact Nat.zero_le _

Although in mathlib there would be le_mul_iff_one_le_right but you're trying to do this in core if I understood correctly.

[Siddharth Bhat]

Aha, thanks!