proposition: Fact lb_mask_meet a b : a ⪯ b <-> a↓b ≂ a.
proof: Proof. split. + intros H; split; auto. induction H as [ | | x y ? ? H ]. * constructor. * rewrite lb_meet_left; constructor; auto. * rewrite lb_meet_cons; constructor; auto. revert x y H; intros [] []; simpl; auto. + intros (H1 & H2). apply lb_mask_trans with (1 := H2). rewrite lb_meet_comm; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)