proposition: Lemma nodup_sort_strict : forall B S (mb : list B) (HL : nodup mb), sort (S%) mb -> sort S mb.
proof: Proof. intros. induction mb. apply nil_sort. gen HL; intro. simpl in HL0. inversion H; subst. assert (sort S mb). tauto. clear IHmb. apply cons_sort; auto. apply nodup_lelistA_strict; auto. Qed.
imports: Coq(List Morphisms Lia) CoLoR(RelUtil LogicUtil) CoLoR(ListNodup)