proposition: Fact lb_ortho_mask_nil a x : a ⟂ x -> x ⪯ a -> x ≂ nil.
proof: Proof. induction 1 as [ | | x y l m H1 H2 IH2 ]; auto. + split; auto. + intros H. apply lb_mask_inv_cons in H; destruct H as (H3 & H4). rewrite IH2; auto; split; auto. revert x y H1 H3. intros [] []; simpl; intros [] ?; try discriminate; constructor; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)