proposition: Lemma GE_prop10l E s: GT E s -> GL E s -> GU E s -> GA E s -> GI E s -> forall x a b, inc x E -> left_inverse E s x a -> left_inverse E s x b -> a = b.
proof: Proof. move => pa pb pc pd pe x a b xE ha hb. 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'). rewrite (GE_prop9 pa pb pc pd pe xE ha ci). by rewrite -(GE_prop9 pa pb pc pd pe xE hb ci). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)