proposition: Fact binary_le_refl x : x ≲ x.
proof: Proof. induction on x as IH with measure x. destruct (eq_nat_dec x 0). + subst; constructor. + constructor 2; auto. apply IH, div_by_p_lt; 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)