proposition: Lemma range_smaller f: fgraph f -> (range f) <=cc (domain f).
proof: Proof. move=> fgf. have ff: (function (triple (domain f) (range f) f)). by apply: function_pr; fprops. have ->: (range f = Imf (triple (domain f)(range f) f)). by rewrite (ImfE ff); aw. by move:(image_smaller ff); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)