proposition: Lemma length_strip : forall (v : list A) (i : nat), i <= length v -> length (strip v i) = length v - i.
proof: Proof. unfold strip in |- *. intros. rewrite length_rev. rewrite length_trunc. trivial with arith. rewrite length_rev. apply minus_le_lem2. Qed.
imports: Arith_compl Minus Lists_compl