proposition: Lemma trunc_strip : forall (v : list A) (i j : nat), trunc (strip v i) j = strip (trunc v (i + j)) i.
proof: Proof. simple induction v. unfold strip in |- *. simpl in |- *. trivial with arith. simple induction i; simple induction j. rewrite trunc_O. rewrite strip_O. auto with arith. intros. rewrite strip_O. rewrite strip_O. auto with arith. rewrite trunc_O. elim plus_n_O. rewrite strip_trunc_i. trivial with arith. intros. rewrite strip_cons_S. replace (S n + S n0) with (S (n + S n0)). simpl in |- *. rewrite strip_cons_S. apply H. auto with arith. Qed.
imports: Arith_compl Minus Lists_compl