proposition: Lemma strip_max : forall (v : list A) (i : nat), length v <= i -> strip v i = nil.
proof: Proof. unfold strip in |- *. intros. rewrite <- rev_eq1. apply rev_eq. rewrite <- length_rev. rewrite minus_le_O. auto with arith. rewrite length_rev. exact H. Qed.
imports: Arith_compl Minus Lists_compl