proposition: Fact pow2_dec_ge1 p b : 1 <= pow2 p*(2*b+1).
proof: Proof. change 1 with (1*1) at 1; apply Nat.mul_le_mono; try lia; apply pow2_ge1. Qed.
imports: List Arith Max Lia Wellfounded Bool Eqdep_dec Undecidability.Shared.Libs.DLW.Utils(list_focus utils_tac utils_list)