proposition: Lemma partition_same y x: partition_w y x -> partition_w_fam (identity_g y) x.
proof: Proof. move=> [un di]; hnf; rewrite setUb_identity. split => //; first by apply: identity_fgraph. hnf; rewrite identity_d => i j iy jy. by rewrite ! identity_ev //; apply: di. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)