proposition: Fact lb_plus_spec a l m : ⟦lb_plus a l m⟧ = bool2nat a + ⟦l⟧ + ⟦m⟧.
proof: Proof. revert a m; induction l as [ | x l IHl ]; intros a m. + rewrite lb_plus_fix_0, lb_succ_spec, lb_nat_fix_0; lia. + destruct m as [ | y m ]. * rewrite lb_plus_fix_1, lb_succ_spec, lb_nat_fix_0; lia. * rewrite lb_plus_fix_2, lb_nat_fix_3, lb_nat_fix_3. destruct a; destruct x; destruct y; simpl; rewrite IHl; simpl; 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)