English
If a' ≤ a, b' ≤ b, c' ≤ c then a' ⨳ b ⨳ c ♯ a ⨳ b' ⨳ c ♯ a ⨳ b ⨳ c' ♯ a' ⨳ b' ⨳ c' ≤ a ⨳ b ⨳ c ♯ a' ⨳ b' ⨳ c ♯ a' ⨳ b ⨳ c' ♯ a ⨳ b' ⨳ c'.
Русский
Если a' ≤ a, b' ≤ b, c' ≤ c, то ... неравенствоnmul_nadd_le₃
LaTeX
$$$\\forall a,b,c,a',b',c' \\in \\mathrm{Ordinal},\\ a' \\le a \\rightarrow b' \\le b \\rightarrow c' \\le c \\rightarrow \\Big( ((a' .nmul b).nmul c).nadd ((a.nmul b').nmul c) \\nadd ((a.nmul b).nmul c')).nadd ((a'.nmul b').nmul c') \\le ((a.nmul b).nmul c).nadd ((a'.nmul b').nmul c)).nadd ((a.nmul b').nmul c')$$$
Lean4
theorem nmul_le_nmul_left (h : a ≤ b) (c) : c ⨳ a ≤ c ⨳ b :=
by
rcases lt_or_eq_of_le h with (h₁ | rfl) <;> rcases (eq_zero_or_pos c).symm with (h₂ | rfl)
· exact (nmul_lt_nmul_of_pos_left h₁ h₂).le
all_goals simp
