Nat.mul_lt_mul0

Stream: Is there code for X?

[Sorawee Porncharoenwase]

Is there

theorem Nat.mul_lt_mul₀ {a b c d : Nat} (h1 : a < c) (h2 : b < d) : a * b < c * d

in the standard library? And if not, is it worth adding it to the stdlib?

FWIW, this is what I have right now (but I'd rather use stdlib instead)

theorem Nat.mul_lt_mul₀ {a b c d : Nat} (h1 : a < c) (h2 : b < d) : a * b < c * d :=
  match b with
  | 0 =>
    match c with
    | 0 => match h1 with .
    | c+1 => by simp [h2]
  | b+1 => Nat.mul_lt_mul h1 (Nat.le_of_lt h2) (by simp)

[Ruben Van de Velde]

Is that Nat.mul_lt_mul h1 h2.le (pos_of_gt h2)?

[Sorawee Porncharoenwase]

I don't think so. Nat.mul_lt_mul requires that 0 < b, but in the above theorem b could be 0, so I don't think a direct application of Nat.mul_lt_mul will work.

[Wrenna Robson]

https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Ring/Defs.html#mul_lt_mul''

[Wrenna Robson]

We don't have a special case for it for Nat, though. Arguably we should.

[Wrenna Robson]

I think there are proofs that use existing lemmas more without the case split. The issue really is that the hypotheses are not tight: using Nat.pos_of_ne_zero and ne_of_lt, you have either 0 < c or 0 < d, and then for either you can just use Nat.mul_lt_mul'.

[Wrenna Robson]

Nat.mul_lt_mul' (le_of_lt h1) h2 (lt_of_le_of_lt (zero_le _) h1) might work?