Lemma location

Stream: maths

[Thomas Browning]

This lemma doesn't seem to be in mathlib, but I'm not sure where it should go. Any suggestions?

@[to_additive] lemma mul_eq_mul_iff_eq_and_eq {N : Type*} [ordered_cancel_comm_monoid N]
  {a b c d : N} (hac : a ≤ c) (hbd : b ≤ d) : a * b = c * d ↔ a = c ∧ b = d :=
begin
  refine ⟨λ h, _, λ h, congr_arg2 (*) h.1 h.2⟩,
  cases eq_or_lt_of_le hac with hac hac,
  { rw hac at h,
    exact ⟨hac, mul_left_cancel h⟩ },
  cases eq_or_lt_of_le hbd with hbd hbd,
  { rw hbd at h,
    exact ⟨mul_right_cancel h, hbd⟩ },
  exact ((mul_lt_mul''' hac hbd).ne h).elim,
end

[Yaël Dillies]

Close to the other ordered_cancel_comm_monoid lemmas, in algebra.order.monoid_lemmas.

[Thomas Browning]

Thanks!

[Antoine Chambert-Loir]

There is something funny: I would have expected that the lemma was missing some exceptional cases where one of the variables is zero, but of course, if it formalizes, it has to be true as stated! (This reminds me of sth that happened to @Sebastien Gouezel in real life.)

[Yaël Dillies]

There is no zero because it's cancel_, which means you can cancel any multiplication: a * b = a * c → b = c