proposition: Lemma Lg_range p x: range (Lg x p) = fun_image x p.
proof: Proof. set_extens z. by move/funI_P=> [a /funI_P [b ib ->] ->]; aw; apply:funI_i. move/funI_P => [b ba ->];apply/funI_P. by exists (J b (p b));aw => //; apply: Lg_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)