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. move: (all_der_p9 ox oy oi oj) (all_der_p10 ox oy oi oj) => ha hb. case: (equal_or_not (g x i) (g y j)) => h2. move/ha:(h2) => [sa sb sc]. split => // _. split => // h3. + rewrite - (sa h3); fprops. + rewrite - (sb h3); fprops. + rewrite - (sc h3); fprops. by rewrite h2; apply: oleR; apply:OS_all_der. split => h. move/hb: (conj h h2) => [sa sb sc]. split => // h3. + exact: (proj1 (sa h3)). + exact: (proj1 (sb h3)). + exact: (proj1 (sc h3)). have[//]: g x i <o g y j. move:h => [sa sb sc]. apply/ hb; split => // h3; split; fprops => ne; case h2; apply /ha. + split => //. by move => ii; move: (proj2 h3); rewrite ii. by move => [/(oltNge h3)]. + by rewrite h3; split => // [] []. + split => //. by move => [/(oltNge h3)]. by move => ii; move: (proj2 h3); rewrite ii. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)