proposition: Fact lb_join_dio a b c : a ≂ b↑c <-> exists x, a ≂ b⊕x /\ b ⪯ b⊕x /\ x ⪯ c /\ c ⪯ a.
proof: Proof. split. + intros H. destruct (@lb_minus_plus b a) as (x & H1 & H2). { rewrite H; auto. } exists x; repeat (split; auto). 2: rewrite H; auto. rewrite <- lb_ortho_plus in H2. rewrite lb_ortho_plus_join in H1; auto. rewrite lb_ortho_meet_nil in H2. rewrite <- (lb_meet_join_idem x b), lb_join_comm. rewrite <- H1, H, lb_meet_join_distr, (lb_meet_comm _ b), H2. rew lb. + intros (x & H1 & H2 & H3 & H4). rewrite <- lb_ortho_plus in H2. rewrite lb_ortho_plus_join in H1; auto. rewrite lb_ortho_meet_nil in H2. split. * rewrite H1; apply lb_join_mono; auto. * apply lb_join_spec; auto; rewrite H1; 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)