proposition: Lemma GE_prop11l E s: GT E s -> GL E s -> GU E s -> GA E s -> GI E s -> forall x, inc x E -> left_inverse E s x (inverse E s x).
proof: Proof. move => pa pb pc pe pd x xE. set p := (fun x' => (VL s) x' x = un E s ). have ha: exists2 x', inc x' E & p x'. move:(GE_prop8l pa pb pc pd xE)=> [a [a1 a2]]; ex_tac. have hb: singl_val2 (inc^~ E) p. move => a b aE pra bE prb. exact:(GE_prop10l pa pb pc pe pd xE (conj aE pra) (conj bE prb)). by move:(select_pr ha hb)=> [hc hd]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)