proposition: Lemma orsum_sr: substrate (order_sum r g) = sum_of_substrates g.
proof: Proof. rewrite /order_sum graph_on_sr // => a asg. have [qudg puv pu] := (du_index_pr1 asg). by right; split => //;move: osa =>[_ _ alo];move: (alo _ qudg) => ou; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)