proposition: Lemma mutually_disjoint_prop1 f: function f -> (forall i j y, inc i (source f) -> inc j (source f) -> inc y (Vf f i) -> inc y (Vf f j) -> i = j) -> mutually_disjoint (graph f).
proof: Proof. by move=> ff hyp; apply: mutually_disjoint_prop; rewrite domain_fg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)