proposition: Fact lb_nat_app l m : lb_nat (l++m) = lb_nat l + (power (length l) 2)*(lb_nat m).
proof: Proof. induction l as [ | x l IHl ]. + rewrite lb_nat_fix_0; simpl; lia. + simpl app; do 2 rewrite lb_nat_fix_3. simpl length; rewrite power_S. rewrite IHl; ring. 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)