proposition: Lemma remove_length_le : forall l x, length (remove x l) <= length l.
proof: Proof. intro l; induction l as [|y l IHl]; simpl; intros x; trivial. destruct (eq_dec x y); simpl. - rewrite IHl; constructor; reflexivity. - apply (proj1 (Nat.succ_le_mono _ _) (IHl x)). Qed.
imports: PeanoNat