proposition: Theorem lb_meet_dio a b c : a ≂ b↓c <-> exists x y, b ≂ a⊕x /\ c ≂ a⊕y /\ a ⪯ a⊕x /\ a ⪯ a⊕y /\ x ⪯ x⊕y.
proof: Proof. split. + intros H. destruct (@lb_minus_plus a b) as (x & H1 & H2). { rewrite H; auto. } destruct (@lb_minus_plus a c) as (y & H3 & H4). { rewrite H; auto. } exists x, y; repeat (split; auto). rewrite <- lb_ortho_plus in H2, H4 |- *. rewrite lb_ortho_plus_join in H1, H3; auto. apply lb_ortho_meet_nil. apply lb_ortho_mask_nil with (a := a). - revert H4; apply lb_ortho_anti; auto. - rewrite H, H1, H3. apply lb_meet_mono; auto. + intros (x & y & H1 & H2 & H3 & H4 & H5). rewrite <- lb_ortho_plus in H3, H4, H5. rewrite H1, H2. do 2 (rewrite lb_ortho_plus_join; auto). rewrite <- lb_join_meet_distr. rewrite lb_ortho_meet_nil in H5. rewrite H5; rew lb. 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)