proposition: Fact lb_succ_spec_1 l : ⟦lb_succ ⟙ l⟧ = S ⟦l⟧.
proof: Proof. induction l as [ | [] ]; auto. + simpl lb_succ; rewrite lb_nat_fix_2. rewrite lb_nat_fix_1, IHl; lia. + simpl lb_succ; rewrite lb_nat_fix_2. rewrite lb_nat_fix_1, lb_succ_spec_0; lia. 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)