proposition: Theorem nat_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. unfold nat_meet. rewrite equal_lb_mask_equiv, nat_lb_nat. rewrite lb_meet_dio. split; intros (x & y & H1 & H2 & H3 & H4 & H5). + exists ⟦x⟧, ⟦y⟧. revert H1 H2 H3 H4 H5. repeat rewrite lb_mask_equiv_equal. repeat rewrite lb_mask_eq_binary_le. repeat rewrite lb_plus_spec_0. repeat rewrite lb_nat_lb; auto. + exists ⟬ x⟭, ⟬ y⟭ . repeat rewrite lb_mask_equiv_equal. repeat rewrite lb_mask_eq_binary_le. rewrite H1, H2. repeat rewrite lb_plus_spec_0. repeat rewrite lb_nat_lb. 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)