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