proposition: Lemma compose_permt g g' et : {h | permt h et = permt g (permt g' et)}.
proof: Proof. have inj_gg': injective (g \o g') by apply: inj_comp; apply: permc_inj. have [|h Dh] := color_inj_permc inj_gg'; first by rewrite /= !permc0. by rewrite -[permt g _]map_comp; exists h; apply/esym/eq_map. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype)