proposition: Lemma GE_prop9 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 -> right_inverse E s x b -> a = b.
proof: Proof. move => pa pb pc ax pd. move: (GE_prop7 pa pb pc)=>[uE up] x a b xE [aE ai] [bE bi]. move/(GE_prop4 pa pb): ax => ac. by move: (ac _ _ _ aE xE bE); rewrite ai bi (proj2 (up _ aE)) (proj1 (up _ bE)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)