proposition: Fact lb_ortho_anti_left a b x : a ⪯ b -> b ⟂ x -> a ⟂ x.
proof: Proof. intros H; revert H x. induction 1 as [ l | m H1 IH1 | x y l m H1 H2 IH2 ]; intros z H3; try (constructor; fail); destruct z as [ | v z ]; try (constructor; fail). + constructor; auto; apply IH1; constructor. + apply lb_ortho_cons_inv in H3. destruct H3 as (H3 & H4). constructor; auto. revert x y v H1 H3. intros [] [] []; simpl; auto. Qed.
imports: List Lia Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac)