proposition: Fact lb_join_inc_left a b : a ⪯ a↑b.
proof: Proof. revert b; induction a as [ | x a IHa ]; intros b. + constructor. + destruct b as [ | y b ]. * rewrite lb_join_left; auto. * rewrite lb_join_cons. apply lb_mask_leb; auto. destruct x; destruct y; simpl; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)