proposition: Lemma GE_prop13a E s: GT E s -> GL E s -> GU E s -> GA E s -> (forall x, inc x E -> exists y, left_inverse E s x y /\ right_inverse E s x y) -> GI E s.
proof: Proof. move => ha hb hc hd hx a b aE bE. move: (hx _ aE) => [c [[cE cp] [_ dp]]]. have ll:= (GE_prop2 ha hb). have st := (GE_prop2_stable ha hb). move/ (GE_prop4 ha hb): hd => asc. move: (GE_prop7 ha hb hc) => [uE up]. move: (up b bE) => [ul ur]. move: (asc _ _ _ aE cE bE); rewrite dp ul => bv. move:(asc _ _ _ bE cE aE); rewrite cp ur => bv2. move: (st _ _ cE bE) (st _ _ bE cE) => dce bde. split. by exists(VL s c b) => //; rewrite - {2} bv; apply:(Law_in ll). by exists(VL s b c) => //; rewrite {2} bv2; apply:(Law_in ll). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)