proposition: Fact nat_lb_fix_0 : ⟬ 0⟭ = nil.
proof: Proof. apply g_nlb_fun with 0; auto; constructor. 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)