proposition: Lemma combine_cons : forall {A B} a b (xs:list A) (ys:list B), combine (a :: xs) (b :: ys) = (a,b) :: combine xs ys.
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