proposition: Lemma flat_map_cons {A B} (f : A -> list B) (x : A) (xs : list A) : flat_map f (x :: xs) = (f x ++ flat_map f xs)%list.
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