proposition: Lemma le_length_strip : forall (v : list A) (i : nat), length (strip v i) <= length v - i.
proof: Proof. unfold strip in |- *. intros. rewrite length_rev. apply le_length_trunc. Qed.
imports: Arith_compl Minus Lists_compl