proposition: Lemma pcan_pickleK sT f f' : @pcancel T sT f f' -> pcancel (pickle \o f) (pcomp f' unpickle).
proof: Proof. by move=> fK x; rewrite /pcomp pickleK /= fK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)