English
Concatenating a new last element on the left and then appending a right series is the same as appending the right series first and then adding the new last on the right.
Русский
Соединение нового последнего элемента слева и добавление справа совпадает с последовательным добавлением справа и затем добавлением нового элемента справа.
LaTeX
$$For p q : RelSeries r and x : α with hx : x ~[r] p.head and hq : p.last ~[r] q.head, (p.cons x hx).append q = (p.append q hq).cons x$$
Lean4
theorem append_cons {p q : RelSeries r} {x : α} (hx : x ~[r] p.head) (hq : p.last ~[r] q.head) :
(p.cons x hx).append q (by simpa) = (p.append q hq).cons x (by simpa) :=
by
simp only [cons]
rw [append_assoc]
