English
If M ≺ N and N ≺ P in the Dershowitz–Manna order, then M ≺ P.
Русский
Если M ≺ N и N ≺ P в порядке Дершовиц-Манна, то M ≺ P.
LaTeX
$$$\\forall M,N,P:\\, IsDershowitzMannaLT(M,N)\\to IsDershowitzMannaLT(N,P)\\to IsDershowitzMannaLT(M,P).$$$
Lean4
/-- `IsDershowitzMannaLT` is transitive. -/
theorem trans : IsDershowitzMannaLT M N → IsDershowitzMannaLT N P → IsDershowitzMannaLT M P := by
classical
rintro ⟨X₁, Y₁, Z₁, -, rfl, rfl, hYZ₁⟩ ⟨X₂, Y₂, Z₂, hZ₂, hXZXY, rfl, hYZ₂⟩
rw [add_comm X₁, add_comm X₂] at hXZXY
refine ⟨X₁ ∩ X₂, Y₁ + (Y₂ - Z₁), Z₂ + (Z₁ - Y₂), ?_, ?_, ?_, ?_⟩
· simpa [-not_and, not_and_or] using .inl hZ₂
· rwa [← add_assoc, add_right_comm, inter_add_sub_of_add_eq_add]
· rw [← add_assoc, add_right_comm, add_left_inj, inter_comm, inter_add_sub_of_add_eq_add]
rwa [eq_comm]
simp only [mem_add, or_imp, forall_and]
refine ⟨fun y hy ↦ ?_, fun y hy ↦ ?_⟩
· obtain ⟨z, hz, hyz⟩ := hYZ₁ y hy
by_cases z_in : z ∈ Y₂
· obtain ⟨w, hw, hzw⟩ := hYZ₂ z z_in
exact ⟨w, .inl hw, hyz.trans hzw⟩
· exact ⟨z, .inr <| by rwa [mem_sub, count_eq_zero_of_notMem z_in, count_pos], hyz⟩
· obtain ⟨z, hz, hyz⟩ := hYZ₂ y <| mem_of_le (Multiset.sub_le_self ..) hy
exact ⟨z, .inl hz, hyz⟩
