proposition: Lemma orsum_pr1: forall i, inc i (domain g) -> exists2 y, inc y (Vg (fam_of_substrates g) i) & inc (J y i) (substrate (order_sum r g)).
proof: Proof. move: (oa) => [_ sr _] i idg; rewrite - sr in idg. rewrite orsum_sr //; apply: (orsum_pr0 idg). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)