proposition: Fact lb_ortho_meet_nil x y : x ⟂ y <-> x↓y ≂ nil.
proof: Proof. split. + intros H; split; try constructor; revert H. induction 1 as [ m | l | x y l m ]. - rewrite lb_meet_right; constructor. - rewrite lb_meet_left; constructor. - rewrite lb_meet_cons. simpl; destruct H; [ destruct y | destruct x ]; try discriminate; subst; simpl; constructor; auto. + intros [ H1 _ ]; revert H1. revert y; induction x as [ | x l IHl ]; intros [ | y m ]; simpl; intros H; try (constructor; fail). destruct x; destruct y; simpl in H |- *; try (inversion H; fail); apply lb_mask_inv_nil in H; constructor; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)