proposition: Fact lb_ortho_join a x y : a ⟂ x↑y <-> a ⟂ x /\ a ⟂ y.
proof: Proof. do 3 rewrite lb_ortho_meet_nil; split. + intros H; apply lb_join_nil_eq. rewrite <- lb_meet_join_distr, H; auto. + intros (H1 & H2). rewrite lb_meet_join_distr, H1, H2; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)