proposition: Fact binary_le_inv n m : n ≲ m -> n = 0 \/ div n 2 ≲ div m 2 /\ rem n 2 <= rem m 2.
proof: Proof. inversion 1; 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)