proposition: Lemma remove_length_lt : forall l x, In x l -> length (remove x l) < length l.
proof: Proof. intro l; induction l as [|y l IHl]; simpl; intros x Hin. - contradiction Hin. - destruct Hin as [-> | Hin]. + destruct (eq_dec x x); [|easy]. apply Nat.lt_succ_r, remove_length_le. + specialize (IHl _ Hin); destruct (eq_dec x y); simpl; auto. now apply Nat.succ_lt_mono in IHl. Qed.
imports: PeanoNat