proposition: Lemma etp_coP f g : g \coP f -> (\Pof g) \coP (\Pof f).
proof: Proof. move => [ha hb hc];split => //. - by apply: etp_f; case: ha. - by apply: etp_f; case: hb. - by rewrite /extension_to_parts; aw; rewrite hc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)