proposition: Fact lb_mask_app l m a b : length l = length m -> l ⪯ m -> a ⪯ b -> l++a ⪯ m++b.
proof: Proof. revert m; induction l as [ | x l IHl ]; intros [ | y m ]; try discriminate; auto; simpl; intros H H1 H2. apply lb_mask_inv_cons in H1; destruct H1 as (H1 & H3). constructor 3; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)