proposition: Lemma GE_prop12l E s: GT E s -> GL E s -> GU E s -> GA E s -> GI E s -> forall x y, inc x E -> inc y E -> VL s x (VL s (inverse E s x) y) = y.
proof: Proof. move => pa pb pc pd pe x y xE yE. move: (GE_prop11r pa pb pc pd pe xE) => [ha hb]. move /(GE_prop4 pa pb): pd => asx. by rewrite (asx _ _ _ xE ha yE) hb (proj1(proj2 (GE_prop7 pa pb pc) _ yE)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)