proposition: Lemma imset_trivIset : trivIset fP = trivIset P.
proof: Proof. apply/trivIsetP/trivIsetP => [trivP A B AP BP|]. - rewrite -(imset_disjoint inj_f) -(inj_eq (imset_inj inj_f)). by apply: trivP; rewrite imset_f. - move=> trivP ? ? /imsetP[A AP ->] /imsetP[B BP ->]. by rewrite (inj_eq (imset_inj inj_f)) imset_disjoint //; apply: trivP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)