proposition: Lemma trivIimset J F (P := F @: J) : {in J &, forall i j, j != i -> [disjoint F i & F j]} -> set0 \notin P -> trivIset P /\ {in J &, injective F}.
proof: Proof. move=> tiF notPset0; split=> [|i j Ji Jj /= eqFij]. apply/trivIsetP=> _ _ /imsetP[i Ji ->] /imsetP[j Jj ->] neqFij. by rewrite tiF // (contraNneq _ neqFij) // => ->. apply: contraNeq notPset0 => neq_ij; apply/imsetP; exists i => //; apply/eqP. by rewrite eq_sym -[F i]setIid setI_eq0 {1}eqFij tiF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)