proposition: Lemma noduplicates_length_le : forall l1 l2, noduplicates l1 -> (forall x, mem x l1 -> mem x l2) -> length l1 <= length l2.
proof: Proof. Proof using. Hint Constructors mem. introv NL ML. gen l2. induction l1 as [|a l1']; intros; rew_list. { math. } { inverts NL as HM NL'. sets_eq l2': (remove a l2). forwards H: length_remove_mem a l2. { applys* ML. } rewrite <- EQl2' in H. forwards~: IHl1' l2'. { introv N. tests: (x = a). subst l2'. applys* mem_remove. } math. } Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)