proposition: Fact lb_join_mono l m a b : l ⪯ m -> a ⪯ b -> l↑a ⪯ m↑b.
proof: Proof. intros H1 H2. apply lb_mask_trans with (l↑b). + apply lb_pointwise_mono_left;auto. intros [] [] []; simpl; auto; discriminate. + do 2 rewrite (lb_join_comm _ b). apply lb_pointwise_mono_left;auto. intros [] [] []; simpl; auto; discriminate. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)