proposition: Theorem length_take_and_jump: forall i j (k: nat) s, (if k then 0 else i) + pred k * j <= length s -> length (take_and_jump i j k s) = k * i.
proof: Proof. intros i j k; generalize i j; elim k; simpl; auto; clear i j k. intros k Rec i j s H; rewrite app_length, length_take1; auto with arith. f_equal; auto. apply Rec. generalize H; case k; clear k H Rec. intros; simpl; auto with arith. intros k H; simpl pred. apply Nat.add_le_mono_l with j. rewrite (fun x (y: list A) => Nat.add_comm x (length y)). rewrite <- length_jump; auto with arith. rewrite Nat.add_shuffle3; auto. apply Nat.le_trans with (2 := H); auto with arith. pattern j at 1; replace j with (0 + (j + 0)); auto with arith. apply Nat.add_le_mono; simpl; auto with arith. simpl; auto with arith. apply Nat.le_trans with (2 := H); auto with arith. Qed.
imports: List ListAux UList OrderedList