proposition: Theorem lap_add_map2 : ∀ β (f g : β → α) la, (List.map f la + List.map g la = List.map (λ b, (f b + g b)%K) la)%lap.
proof: Proof. intros β f g la. induction la as [| b]; [ reflexivity | simpl ]. constructor; auto with Arith. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation