proposition: Fact lb_mask_join a b : a ⪯ b <-> a↑b ≂ b.
proof: Proof. split. + intros H; split. 2: rewrite lb_join_comm; auto. induction H as [ | | x y ? ? H ]. * rewrite lb_join_right; auto. * rewrite lb_join_left; constructor; auto. * rewrite lb_join_cons; constructor; auto. revert x y H; intros [] []; simpl; auto. + intros (H1 & _). apply lb_mask_trans with (2 := H1); auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)