fact: Fixpoint lap_add {α} {r : ring α} al₁ al₂ := match al₁ with | [] => al₂ | [a₁ … bl₁] => match al₂ with | [] => al₁ | [a₂ … bl₂] => [(a₁ + a₂)%K … lap_add bl₁ bl₂] end end.
imports: Utf8 QArith NPeano Misc Field2 Fsummation