proposition: Lemma binary_le_eq_lb_mask x y : x ≲ y <-> ⟬ x⟭ ⪯ ⟬ y⟭ .
proof: Proof. split; auto. intro; rewrite <- (lb_nat_lb x), <- (lb_nat_lb y); 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)