proposition: Lemma oprod_set0 r g: domain g = emptyset -> oprod r g = \1o.
proof: Proof. move=> dge. rewrite/oprod/Lgcomp dge /Lg funI_set0/order_prod /graph_on. have [y ->]: singletonp (prod_of_substrates emptyset). by apply: setX_set1; hnf;rewrite /fam_of_substrates; aw => t/in_set0. set s1 := Zo _ _. suff: s1 = singleton (J y y) by move => ->; exact:ordinal1_pr. apply:set1_pr. apply: Zo_i; first by apply: setXp_i; apply /set1_P. move => j []; rewrite domain_set0 Zo_empty induced_order_empty. by rewrite (proj2 set0_wor) => /in_set0. by move => z /Zo_S /setX_P [pz /set1_P pa /set1_P pb]; rewrite - pz pa pb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)