proposition: Lemma In_length_remove : forall (x : A) l, In x l -> length (remove x l) < length l.
proof: Proof. induction l; simpl; intros. contr. destruct (eq_dec a x). apply NatCompat.le_lt_n_Sm. apply length_remove. destruct H. rewrite H in n. tauto. simpl. apply NatCompat.lt_n_S. apply IHl. hyp. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)