proposition: Fact lb_meet_dec_left a b : a↓b ⪯ a.
proof: Proof. revert b; induction a as [ | x a IHa ]; intros b. + rewrite lb_meet_right; constructor. + destruct b as [ | y b ]. * rewrite lb_meet_left; constructor. * rewrite lb_meet_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)