proposition: Fact binary_le_join_inv m a b : m ≲ a⇡b -> m = (m⇣a)⇡(m⇣b).
proof: Proof. rewrite binary_le_nat_meet, nat_meet_join_distr_l; 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)