proposition: Lemma combine_tail : forall A (l1 l2: list A), combine (tail l1) (tail l2) = tail (combine l1 l2).
proof: Proof. intros A l1 l2;functional induction (combine l1 l2). vm_compute;reflexivity. simpl;destruct tl; reflexivity. simpl;reflexivity. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)