proposition: Fact lb_mask_trans l m k : l ⪯ m -> m ⪯ k -> l ⪯ k.
proof: Proof. intros H1; revert H1 k. induction 1 as [ l | l H1 IH1 | x y l m H1 IH1 ]. + intros; constructor. + intros [ | z k ] Hk. * constructor; auto. * constructor; simpl; auto; apply IH1; constructor. + intros [ | z k ] Hk. * apply lb_mask_inv_left in Hk; destruct Hk as (? & Hk); subst y. destruct x; simpl in H1; try discriminate. constructor; auto. * apply lb_mask_inv_cons in Hk. destruct Hk as (H2 & Hk). constructor; auto. revert x y z H1 H2. intros [] [] []; simpl; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)