proposition: Lemma funI_P f x y: inc y (fun_image x f) <-> exists2 z, inc z x & y = f z.
proof: Proof. split; last by move=> [a ax ->]; apply:funI_i. case/IM_P => a ->; exists (Ro a) => //; apply: R_inc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)