proposition: Lemma combine_nil_r : forall {A B} (xs:list A), combine xs (@nil B) = nil.
proof: Proof. destruct xs; 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