proposition: Lemma osum_set0 r g: domain g = emptyset -> osum r g = \0o.
proof: Proof. move=> dge. rewrite /osum /Lgcomp dge /Lg funI_set0 /order_sum ; set r' := graph_on _ _. suff: r' = emptyset by move => ->; exact ordinal0_pr. apply/set0_P => t /Zo_S /setX_P [_ _] /du_index_pr1; rewrite domain_set0. by move => [/in_set0]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)