proposition: Lemma sub_fgraph f g: fgraph g -> sub f g -> fgraph f.
proof: Proof. move=> [fg ffg] s; split. by move=> t tf; apply: (fg _ (s _ tf)). by move=> x y xf yf; apply: ffg; apply: s. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)