proposition: Lemma NoDup_incl_length l l' : NoDup l -> incl l l' -> length l <= length l'.
proof: Proof. intros N. revert l'. induction N as [|a l Hal N IH]; simpl. - intros. now apply Nat.le_0_l. - intros l' H. destruct (Add_inv a l') as (l'', AD). { apply H; simpl; auto. } rewrite (Add_length AD). apply le_n_S. apply IH. now apply incl_Add_inv with a l'. Qed.
imports: PeanoNat