proposition: Lemma strip_strip_S : forall (v : list A) (i j : nat), strip (strip v (S i)) j = strip (strip v i) (S j).
proof: Proof. simple induction v. intros. rewrite strip_nil. rewrite strip_nil. trivial with arith. simple induction i. intros. rewrite strip_O. do 2 rewrite strip_cons_S. rewrite strip_O. trivial with arith. simple induction j. rewrite strip_O. repeat rewrite strip_cons_S. elim n. rewrite strip_O. trivial with arith. intros. rewrite <- H. rewrite strip_O. trivial with arith. intros. do 2 rewrite strip_cons_S. apply H. Qed.
imports: Arith_compl Minus Lists_compl