proposition: Lemma noduplicates_two : forall (x y:A), x <> y -> noduplicates (x::y::nil).
proof: Proof. Proof using. intros. applys noduplicates_cons. { intros M. rewrite mem_one_eq in M. false. } applys noduplicates_one. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)