proposition: Lemma sum_enum_uniq : uniq sum_enum.
proof: Proof. rewrite cat_uniq -!enumT !(enum_uniq, map_inj_uniq); try by move=> ? ? []. by rewrite andbT; apply/hasP=> [[_ /mapP[x _ ->] /mapP[]]]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)