proposition: Lemma length_remove_mem : forall x l, mem x l -> length (remove x l) < length l.
proof: Proof. Proof using. unfold remove. intros x l. induction l; rew_listx; introv M. { false. } { case_if; rew_list. { destruct M; tryfalse. forwards~: IHl. math. } { lets: length_filter l (<> x). math. } } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)