proposition: Lemma set_of_graphs_pr x y z: inc z (sub_functions x y) -> inc (graph z) (fgraphs x y).
proof: Proof. move => /sfunctionsP [ff sf <-]; apply/fgraphsP. by move: (f_range_graph ff) => rr; case ff => _ qa <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)