proposition: Fact binary_le_zero_inv n : n ≲ 0 -> n = 0.
proof: Proof. intros H; apply binary_le_le in H; lia. 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)