proposition: Lemma GE_prop8l E s: GT E s -> GL E s -> GU E s -> GI E s -> forall x, inc x E -> exists a, left_inverse E s x a.
proof: Proof. move => type law inv R4 x xE. move: (proj1(GE_prop7 type law inv)) => unp. move: (R4 _ _ xE unp) => [_ [z ha hb]]; exists z => //. by move: (Law_val (GE_prop2 type law) hb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)