fact: Definition lap_compose2 {α} {r : ring α} la lb := List.fold_right (λ i accu, lap_add accu (lap_mul [List.nth i la 0] (lap_power lb i)))%K [] (List.seq 0 (length la)).
imports: Utf8 QArith NPeano Misc Field2 Fsummation