proposition: Fact binary_le_le x y : x ≲ y -> x <= y.
proof: Proof. induction 1 as [ n | n m H1 H2 IH2 ]; try lia. rewrite (div_rem_spec1 n 2), (div_rem_spec1 m 2); 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)