proposition: Fact lb_succ_spec a l : ⟦lb_succ a l⟧ = bool2nat a + ⟦l⟧.
proof: Proof. destruct a. + rewrite lb_succ_spec_1; auto. + rewrite lb_succ_spec_0; 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)