proposition: Lemma transport_inv E F g s x y: bijection_prop g E F -> GT E s -> GL E s -> GU E s -> inc x E -> left_inverse E s x y -> left_inverse F (transport s g) (Vf g x) (Vf g y).
proof: Proof. move => bg ha hb hc xE [yE xy]. move:(bg) => [[[fg gi] [_ gs]] sg tg]. rewrite sg in gi gs; rewrite tg in gs. have xF: inc (Vf g x) F by Wtac. have yF: inc (Vf g y) F by Wtac. split => //; rewrite(transport_un bg ha hb hc). by rewrite - (transport_op bg ha hb yE xE) xy. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)