proposition: Lemma nodup_incl_length_le : forall l m : list A, nodup l -> l [= m -> length l <= length m.
proof: Proof. induction l; simpl; intros m l_nodup lm. lia. destruct l_nodup as [a_notin_l l_nodup]. assert (am : In a m). apply lm. fo. destruct (in_elim am) as [m1 [m2 e]]. subst. assert (lm1m2 : l [= m1 ++ m2). intros x xl. assert (xal : In x (a :: l)). right. hyp. apply lm in xal. rewrite in_app in xal. assert (x <> a). intro. subst. contr. firstorder auto with datatypes exfalso. gen (IHl _ l_nodup lm1m2). rewrite !app_length. simpl. lia. Qed.
imports: CoLoR(ListUtil NatUtil RelMidex LogicUtil)