proposition: Lemma GE_prop11r E s: GT E s -> GL E s -> GU E s -> GA E s -> GI E s -> forall x, inc x E -> right_inverse E s x (inverse E s x).
proof: Proof. move => pa pb pc pd pe x xE. move: (GE_prop11l pa pb pc pd pe xE) => ha. move: (pe _ _ xE (proj1 (GE_prop7 pa pb pc))) => [[c ha' hb'] _]. have ci: right_inverse E s x c. by split => //;move: (Law_val (GE_prop2 pa pb) hb'). by move:(GE_prop9 pa pb pc pd pe xE ha ci) => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)