English
If a ≤ b and c ≤ d in a commutative ordered monoid with monotone multiplications, then the product Icc(a,b)·Icc(c,d) equals Icc(ac, bd).
Русский
Если a ≤ b и c ≤ d в коммутативной упорядоченной монаде, то Icc(a,b)·Icc(c,d) = Icc(ac,bd).
LaTeX
$$$$ Icc(a,b) \\cdot Icc(c,d) = Icc(a c, b d) \\\\text{ при } a \\le b,\\; c \\le d. $$$$
Lean4
@[to_additive]
theorem Icc_mul_Icc (hab : a ≤ b) (hcd : c ≤ d) : Icc a b * Icc c d = Icc (a * c) (b * d) :=
by
refine (Icc_mul_Icc_subset' _ _ _ _).antisymm fun x ⟨hacx, hxbd⟩ ↦ ?_
obtain hxbc | hbcx := le_total x (b * c)
· obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le hacx
refine ⟨a * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, c, left_mem_Icc.2 hcd, mul_right_comm ..⟩
rwa [mul_right_comm, mul_le_mul_iff_right] at hxbc
· obtain ⟨y, hy, rfl⟩ := exists_one_le_mul_of_le hbcx
refine ⟨b, right_mem_Icc.2 hab, c * y, ⟨le_mul_of_one_le_right' hy, ?_⟩, (mul_assoc ..).symm⟩
rwa [mul_assoc, mul_le_mul_iff_left] at hxbd
