proposition: Fact lb_ortho_anti a b x y : a ⪯ b -> x ⪯ y -> b ⟂ y -> a ⟂ x.
proof: Proof. intros H1 H2 H3. apply lb_ortho_anti_left with (1 := H1), lb_ortho_sym, lb_ortho_anti_left with (1 := H2), lb_ortho_sym. trivial. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)