proposition: Lemma empty_source_graph f: function f -> source f = emptyset -> graph f = emptyset.
proof: Proof. move => ff sfe; apply /set0_P => x xp. apply: (@in_set0 (P x)); rewrite - sfe; Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)