proposition: Lemma strip_strip : forall (v : list A) (i j : nat), strip (strip v i) j = strip v (i + j).
proof: Proof. simple induction v. intros. rewrite strip_nil. rewrite strip_nil. trivial with arith. simple induction i. intro. simpl in |- *. rewrite strip_O. trivial with arith. simple induction j. rewrite strip_O. elim plus_n_O. trivial with arith. intros. rewrite strip_cons_S. simpl in |- *. rewrite strip_cons_S. apply H. Qed.
imports: Arith_compl Minus Lists_compl