proposition: Lemma jump_length : forall A n (l1 l2:list A), length l1 = length l2 -> length (jump n l1) = length (jump n l2).
proof: Proof. intros A n l1;functional induction (jump n l1); simpl; intros l2 Hlength. apply IHl0; apply IHl; apply tail_length; apply Hlength. apply IHl0; apply IHl; apply Hlength. apply tail_length; apply Hlength. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)