proposition: Lemma all_der_p10 x y i j: ordinalp x -> ordinalp y -> ordinalp i -> ordinalp j -> (g x i <o g y j <-> [/\ i <o j -> x <o g y j, i = j -> x <o y & j <o i -> g x i <o y]).
proof: Proof. move => ox oy oi oj. case (oleT_ell oi oj). + move => ->; split. by move /(all_der_p5'' oj ox oy) => h; split => // [][]. move => [_ ok _]; exact: (all_der_p5 oj (ok (erefl j))). + move => lij. move: (all_der_p7 oy lij) => eq1. split. rewrite - {1} eq1; move /(all_der_p5'' oi ox (OS_all_der oy oj)) => h1. split => //. - by move => ii; move: (proj2 lij); rewrite ii. - by move => [/(oltNge lij)]. - by move => [h _ _]; rewrite - eq1; apply:all_der_p5 => //; apply:h. + move => lji. move: (all_der_p7 ox lji) => eq1. split. rewrite - {1} eq1; move /(all_der_p5'' oj (OS_all_der ox oi) oy) => h1. split => //. - by move => [/(oltNge lji)]. - by move => ii; move: (proj2 lji); rewrite ii. - by move => [_ _ h]; rewrite - eq1; apply:all_der_p5 => //; apply:h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)