proposition: Lemma equivalence_partitionP : partition P D.
proof: Proof. have defD: cover P == D. rewrite eqEsubset; apply/andP; split. by apply/bigcupsP=> _ /imsetP[x Dx ->]; rewrite /Px setIdE subsetIl. by apply/subsetP=> x Dx; apply/bigcupP; exists (Px x); rewrite (Pxx, PPx). have tiP: trivIset P. apply/trivIsetP=> _ _ /imsetP[x Dx ->] /imsetP[y Dy ->]; apply: contraR. case/pred0Pn=> z /andP[] /[!inE] /andP[Dz Rxz] /andP[_ Ryz]. apply/eqP/setP=> t /[!inE]; apply: andb_id2l => Dt. by rewrite (eqiR Dx Dz Dt) // (eqiR Dy Dz Dt). rewrite /partition tiP defD /=. by apply/imsetP=> [[x /Pxx Px_x Px0]]; rewrite -Px0 inE in Px_x. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)