proposition: Lemma all_mem_pos_jump : forall n (l:list Z), all_mem_pos l -> all_mem_pos (jump n l).
proof: Proof. intros n l;functional induction (jump n l);simpl;intros Hmem. apply IHl1;apply IHl0;apply all_mem_pos_tail; apply Hmem. apply IHl1;apply IHl0;apply Hmem. apply all_mem_pos_tail; apply Hmem. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)