proposition: Lemma length_remove : forall (x : A) l, length (remove x l) <= length l.
proof: Proof. induction l; simpl; intros. apply Nat.le_0_l. destruct (eq_dec a x). apply Nat.le_trans with (length l). apply IHl. apply Nat.le_succ_diag_r. simpl. apply le_n_S. apply IHl. Qed.
imports: CoLoR(LogicUtil EqUtil RelUtil BoolUtil NatUtil) Coq(Setoid SetoidList FunInd)