proposition: Lemma orsum2_greatest r r' x: order r -> order r' -> ne_substrate r' -> greatest (order_sum2 r r') x -> greatest r' (P x).
proof: Proof. move=> or or' [y ysr] [xsp xgr]. have aux: forall z, inc z (substrate r') -> (inc (J z C1) (substrate (order_sum2 r r'))). by move => z zi; rewrite (orsum2_sr or or'); apply: candu2_prb. move: (xgr _ (aux _ ysr)) => /orsum2_gleP; aw; move => [_ p1 p2]. move: p1 => /candu2P [px]; case => [] [pxs qxb]. by case: p2=> [] [p1 p3];[case: C1_ne_C0| case: p3| case: C1_ne_C0]. split => // x0 x0sr;move /orsum2_gleP:(xgr _ (aux _ x0sr)); aw;move=> [q1 q2]. by have D :=C1_ne_C0; case;case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)