proposition: Theorem remSizeLess : forall (a : A) (L : list A), In a L -> length (rem a L) < length L.
proof: Proof. intros a L; elim L; simpl in |- *; auto. intros H'; elim H'. intros a0 l H' H'0; case (ADec a a0); simpl in |- *; auto with datatypes. intros H'1; case (In_dec ADec a l); auto with arith. intros H'2; rewrite remEq; auto. intros H'1; case H'0; auto with arith. intros H'2; case H'1; auto. Qed.
imports: Coq(Arith) Coq(List)