proposition: Lemma orsum2_greatest' r r' x: order r -> order r' -> greatest r' x -> greatest (order_sum2 r r') (J x C1).
proof: Proof. move => or1 or2 [pa pb]. have xx:= (candu2_prb (substrate r)pa). hnf; rewrite (orsum2_sr or1 or2); split; first exact. move => y yd; apply /orsum2_gleP; split ; [exact | exact | ]. move/candu2P: yd => [py]; case; move => [l1 l2]. constructor 3; aw; split;fprops. constructor 2; aw; rewrite l2;split;fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)