proposition: Fact lb_minus_plus a b : a ⪯ b -> exists x, b ≂ a⊕x /\ a ⪯ a⊕x.
proof: Proof. intros H. destruct lb_minus with (1 := H) as (x & H1 & H2). exists x; rewrite lb_ortho_plus_join; auto. Qed.
imports: Arith Nat Lia List Bool Setoid Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list utils_nat bool_list gcd sums power_decomp)