proposition: Fact nat_lb_spec n : g_nlb n (nat_lb n).
proof: Proof. apply (proj2_sig (nat_lb_full _)). 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)