proposition: Lemma strip_trunc : forall (v : list A) (i j : nat), strip (trunc v i) j = trunc (strip v j) (i - j).
proof: Proof. simple induction v. simpl in |- *. unfold strip in |- *. simpl in |- *. trivial with arith. simple induction i; simple induction j. simpl in |- *. rewrite strip_O. rewrite trunc_O. trivial with arith. rewrite trunc_O. simpl in |- *. intros. unfold strip in |- *. simpl in |- *. rewrite trunc_O. trivial with arith. rewrite strip_O. rewrite strip_O. elim minus_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