proposition: Lemma pc_fb: bijection (product_compose f u).
proof: Proof. move: (pc_f)=> fpc. have su: surjection u by move: bu=> [_]. have spc: (source (product_compose f u) = productb f). by rewrite /product_compose; aw. split. split=>//. rewrite spc=> x y xs ys eq. apply: (setXb_exten xs ys). rewrite -tudf; move=> i iu; move: ((proj2 su) _ iu) => [z zs ->]. by rewrite - (pc_VV xs zs) -(pc_VV ys zs) eq. split => //. set nf:= Lg (source u) (fun k => Vg f (Vf u k)). have tpc:target (product_compose f u) = productb nf. by rewrite /product_compose; aw. rewrite tpc spc => y yp. set x:= Lg (domain f) (fun i => Vg y (Vf (inverse_fun u) i)). have xp: (inc x (productb f)). apply: setXb_gi => i id. rewrite -tudf in id; move: ((proj2 su) _ id) => [z zsu wz]. rewrite wz (inverse_V2 bu zsu). move/setXb_P: yp => [fy dy iVV]. by move: (iVV z); rewrite /nf; aw; rewrite LgV //; apply. ex_tac. have Wt: inc (Vf (product_compose f u) x) (productb nf). by rewrite - spc in xp; move: (Vf_target fpc xp); rewrite tpc. symmetry;apply: (setXb_exten Wt yp) => i; rewrite /nf; aw=> id. have Wd: inc (Vf u i)(domain f) by rewrite -tudf; Wtac; fct_tac. rewrite pc_VV // (LgV Wd) (inverse_V2 bu id) //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)