proposition: Lemma noduplicates_rev : forall l, noduplicates l -> noduplicates (rev l).
proof: Proof. Proof using. introv M. apply~ noduplicates_Nth_same. introv N1 N2. lets N1': Nth_rev_inv N1. lets N2': Nth_rev_inv N2. lets I1: Nth_inbound N1. lets I2: Nth_inbound N2. rewrite length_rev in *. lets: noduplicates_Nth_same_inv M N1' N2'. math. Qed.
imports: Coq.Classes.Morphisms TLC(LibTactics LibLogic LibReflect LibOperation LibProd LibOption LibNat LibInt LibWf LibMonoid LibRelation)