proposition: Lemma pointwise_map {A B} : Proper ((pointwise_relation _ eq) ==> eq ==> eq) (@List.map A B).
proof: Proof. repeat intro; cbv [pointwise_relation] in *; subst. match goal with [H:list _ |- _ ] => induction H as [|? IH IHIH] end; [reflexivity|]. simpl. rewrite IHIH. congruence. Qed.
imports: Coq.ZArith.ZArith Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.QArith.QArith_base Coq.QArith.Qreduction Coq.QArith.Qround