proposition: Fact comp_app i ll mm j : comp i (ll++mm) j = comp i ll j ++ comp (length ll+i) mm (lsum ll+j).
proof: Proof. revert i j; induction ll as [ | x ll IH ]; simpl; intros i j; auto. rewrite IH; solve list eq; do 3 f_equal; lia. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode)