proposition: Lemma GE_I_range E : range (GE_I E) = E.
proof: Proof. apply: extensionality => x. by move /funI_P => [z / GE_I_incP [_ <- h] ->]. move=> xe;apply/funI_P; exists (J x x); aw; trivial;apply/GE_I_incP; aw. split => //; apply: pair_is_pair. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)