proposition: Lemma combine_rev : forall r s, length r = length s -> combine (rev r) (rev s) = rev (combine r s).
proof: Proof. Proof using. intros r. induction r; introv E; destruct s; tryfalse. { auto. } { rew_list in *. rewrite combine_last, combine_cons. { rewrite IHr. rew_list~. math. } { rew_list. math. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)