proposition: Lemma orsum2_nc: exists r r', [/\ order r, order r' & ~ ( (order_sum2 r r') \Is (order_sum2 r' r))].
proof: Proof. move: (diagonal_osr (singleton C0))=> []; set r1 := diagonal _ => or1 sr1. move: (diagonal_osr (doubleton C0 C1))=> []; set r2 := diagonal _ => or2 sr2. have ns2: ne_substrate r2. have jp: inc (J C0 C0) r2 by apply /diagonal_pi_P;split;fprops. exists C0; substr_tac. have ng2: forall x, greatest r2 x -> False. move => x [_]; rewrite sr2 => h2;case: C0_ne_C1. move: (h2 _ (set2_1 C0 C1)) (h2 _ (set2_2 C0 C1)). by move /diagonal_pi_P => [_ ->] /diagonal_pi_P [_ ->]. have g2: greatest (order_sum2 r2 r1) (J C0 C1). apply:(orsum2_greatest' or2 or1); red; rewrite sr1; split;fprops. move => x /set1_P ->; apply/diagonal_pi_P;split;fprops. exists r2; exists r1;split => // [] [f isf]. move: (orsum2_greatest or1 or2 ns2 (image_of_greatest isf g2)) => eg. by case: (ng2 (P (Vf f (J C0 C1)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)