English
If l is a maximal product and q is smaller than the tail of l, then the list (term I ho :: q.val) is a chain with respect to the GT relation.
Русский
Если l — максимальный произведение, а q меньше хвоста l, тогда список (term I ho :: q.val) образует цепь по отношению GT.
LaTeX
$$$$\\text{IsChain}_{GT}(\,\\text{term }I\\ ho :: q.\\mathrm{val}\\,).$$$$
Lean4
theorem isChain_cons_of_lt (l : MaxProducts C ho) (q : Products I) (hq : q < l.val.Tail) :
List.IsChain (fun x x_1 ↦ x > x_1) (term I ho :: q.val) :=
by
have : Inhabited I := ⟨term I ho⟩
rw [List.isChain_iff_pairwise]
simp only [gt_iff_lt, List.pairwise_cons]
refine ⟨fun a ha ↦ lt_of_le_of_lt (Products.rel_head!_of_mem ha) ?_, List.isChain_iff_pairwise.mp q.prop⟩
refine lt_of_le_of_lt (Products.head!_le_of_lt hq (q.val.ne_nil_of_mem ha)) ?_
by_cases hM : l.val.Tail.val = []
· rw [Products.lt_iff_lex_lt, hM] at hq
simp only [List.not_lex_nil] at hq
· have := l.val.prop
rw [max_eq_o_cons_tail C hsC ho l, List.isChain_iff_pairwise] at this
exact List.rel_of_pairwise_cons this (List.head!_mem_self hM)
