proposition: Lemma map_cons A B (f : A -> B) (x : A) (l : list A) : List.map f (x :: l) = f x :: List.map f l.
proof: Proof. reflexivity. Qed.
imports: Coq.ZArith.ZArith Coq.Lists.List Coq.Setoids.Setoid Coq.Classes.Morphisms Coq.QArith.QArith_base Coq.QArith.Qreduction Coq.QArith.Qround