proposition: Lemma injective_partition f x: partition_s_fam f x -> injective_graph f.
proof: Proof. move=> [[fgf md ux] hyp]; split=>//. move=> a b ad bd sV; move: (md _ _ ad bd) (hyp _ bd)=> [] //. rewrite /disjoint sV setI2_id => -> [_ [[]]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)