proposition: Lemma app_trunc_strip : forall (v : list A) (i : nat), trunc v i ++ strip v i = v.
proof: Proof. simple induction v. unfold strip in |- *. simpl in |- *. trivial with arith. intros. elim i. rewrite trunc_O. rewrite strip_O. simpl in |- *. trivial with arith. intros. unfold strip in |- *. simpl in |- *. rewrite trunc_app. rewrite rev_app. rewrite length_rev. case n. rewrite <- minus_n_O. rewrite <- minus_n_n. rewrite trunc_O. rewrite trunc_O. simpl in |- *. rewrite <- length_rev. rewrite trunc_all. rewrite rev_rev. trivial with arith. intro. replace (length l - S n0 - length l) with 0. rewrite trunc_O. simpl in |- *. replace (rev A (trunc (rev A l) (length l - S n0))) with (strip l (S n0)). rewrite H. trivial with arith. unfold strip in |- *. trivial with arith. rewrite minus_minus_lem1. trivial with arith. Qed.
imports: Arith_compl Minus Lists_compl