proposition: Lemma identity_r x: range (identity_g x) = x.
proof: Proof. set_extens t; first by move/Lg_range_P => [y yi ->]. by move => tx; apply/Lg_range_P; exists t. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)