proposition: Lemma rangeP r : sgraph r -> forall y, (inc y (range r) <-> (exists x, inc (J x y) r)).
proof: Proof. move=> gr y; split;last by move=> [x]; apply range_i. by case/funI_P => x xr ->; exists (P x); rewrite (gr _ xr). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)