proposition: Lemma length_remove A (A_eq_dec : ∀ x y : A, { x = y } + { x ≠ y }) x xs : (length (remove A_eq_dec x xs) <= length xs)%nat.
proof: Proof. induction xs; auto. simpl. destruct (A_eq_dec x a); subst. apply PeanoNat.Nat.le_le_succ_r, IHxs. simpl. apply le_n_S, IHxs. Qed.
imports: Coq.Lists.List Category.Lib.Tactics