proposition: Theorem lap_add_map : ∀ α β (Rα : ring α) (Rβ : ring β) (f : α → β) la lb, (∀ a b, (f (a + b) = f a + f b)%K) → (List.map f (la + lb) = List.map f la + List.map f lb)%lap.
proof: Proof. clear. intros α β Rα Rβ f la lb Hab. revert lb. induction la as [| a]; intros; [ reflexivity | simpl ]. destruct lb as [| b]; [ reflexivity | simpl ]. rewrite Hab, IHla; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation