proposition: Lemma orsum2_gle_spec x x': inc x (substrate r) -> inc x' (substrate r') -> glt (order_sum2 r r') (J x C0) (J x' C1).
proof: Proof. move=> xsr xsr'; split; last by move => h; move: (pr2_def h); fprops. apply /orsum2_gleP; split; first by apply: candu2_pra. by apply: candu2_prb. constructor 3; aw; split; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)