proposition: Lemma length_le_and_incl_implies_dup_or_perm l m : length l <= length m -> incl m l -> list_has_dup m \/ m ~p l.
proof: Proof. revert m; induction l as [ | x l IHl ]; intros m; simpl; intros H1 H2; auto. + destruct m as [ | y ]; auto; destruct (H2 y); simpl; auto. + destruct incl_right_cons_incl_or_lhd_or_perm with (1 := H2) as [ H3 | [ H3 | (m' & H3 & H4) ] ]; auto. * destruct IHl with (2 := H3) as [ | H ]; try lia; auto. apply Permutation_length in H; lia. * destruct IHl with (2 := H4) as [ H | H ]; try (simpl; lia). - apply Permutation_length in H3; simpl in H3; lia. - left; apply perm_list_has_dup with (1 := Permutation_sym H3). constructor 2; auto. - right; apply perm_trans with (1 := H3); auto. Qed.
imports: Arith Lia List Permutation Relations Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)