proposition: Lemma card_uniqP s : reflect (#|s| = size s) (uniq s).
proof: Proof. elim: s => [|x s IHs]; first by left; apply: card0. rewrite cardU1 /= /addn; case: {+}(x \in s) => /=. by right=> card_Ssz; have:= card_size s; rewrite card_Ssz ltnn. by apply: (iffP IHs) => [<-| [<-]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)