proposition: Fact comp_length i ll j : length (comp i ll j) = lsum ll.
proof: Proof. Proof using Hc. revert i j; induction ll as [ | x ll IH ]; simpl; intros i j; auto. rew length; rewrite IH, Hc; trivial. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils subcode)