proposition: Fact find_pow2_prop x : x <= pow2 (find_pow2 x).
proof: Proof. unfold find_pow2; destruct x. + simpl; lia. + apply loop_prop; auto. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)