proposition: Theorem cprod_Cn X f: target f = domain X -> bijection f -> cprod X = cprod (X \cf (graph f)).
proof: Proof. move=> tF bijf;apply /card_eqP. exists (product_compose X f); hnf;rewrite lf_source lf_target. split => //; [by apply: pc_fb | rewrite /composef domain_fg //; fct_tac]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)