proposition: Lemma imset_trivIset : trivIset P = trivIset fP.
proof: Proof. apply/trivIsetP/trivIsetP. - move=> trivP ? ? /imsetP[A AP ->] /imsetP[B BP ->]. by rewrite (inj_eq imset_inj) imset_disjoint; apply: trivP. - move=> trivP A B AP BP; rewrite -imset_disjoint -(inj_eq imset_inj). by apply: trivP; rewrite imset_f. Qed.
imports: mathcomp(all_ssreflect)