proposition: Lemma transport_inverse E F g s x: bijection_prop g E F -> GT E s -> GL E s -> GA E s -> GU E s -> GI E s -> inc x E -> Vf g (inverse E s x) = inverse F (transport s g) (Vf g x).
proof: Proof. move => bg ha hb hc hd he xE. move:(bg) => [[[fg gi] [_ gs]] sg tg]. rewrite sg in gi gs; rewrite tg in gs. move: (GE_prop11l ha hb hd hc he xE); set ix := inverse _ _ _. move => [pa pb]. have ixf: inc (Vf g ix) F by Wtac. have t1:= (transport_un bg ha hb hd). have ra: VL (transport s g) (Vf g ix) (Vf g x) = un F (transport s g). by rewrite t1 -(transport_op bg ha hb pa xE) pb. apply: select_uniq => // a b /= aF ap bF bp. move:(gs _ aF) (gs _ bF) => [u uE uv] [v vE vv]. have st := (GE_prop2_stable ha hb). move: (proj1 (GE_prop7 ha hb hd)) => iuE. move: ap bp. rewrite uv vv t1 -(transport_op bg ha hb uE xE) => eq1. move:(gi _ _ (st _ _ uE xE) iuE eq1) => iv1. rewrite -(transport_op bg ha hb vE xE) => eq2. move:(gi _ _ (st _ _ vE xE) iuE eq2) => iv2. by congr (Vf g); apply: (GE_prop10l ha hb hd hc he xE). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)