proposition: Lemma strip_app : forall (v1 v2 : list A) (i : nat), strip (v1 ++ v2) i = strip v1 i ++ strip v2 (i - length v1).
proof: Proof. simple induction v1. simpl in |- *. intros. elim minus_n_O. trivial with arith. simple induction v2. intro. simpl in |- *. rewrite strip_nil. rewrite app_v_nil. rewrite app_v_nil. trivial with arith. simple induction i. rewrite strip_O. simpl in |- *. rewrite strip_O. rewrite strip_O. auto with arith. intros. rewrite app_eq2. rewrite strip_cons_S. rewrite strip_cons_S. rewrite length_eq2. simpl in |- *. apply H. Qed.
imports: Arith_compl Minus Lists_compl