proposition: Lemma orsum_gleP x x': gle (order_sum r g) x x' <-> [/\ inc x (sum_of_substrates g), inc x' (sum_of_substrates g) & order_sum_r r g x x'].
proof: Proof. apply: graph_on_P1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)