proposition: Lemma all_der_p5'' x y i: ordinalp i -> ordinalp x -> ordinalp y -> g x i <o g y i -> x<o y.
proof: Proof. move => oi ox oy h. case: (oleT_ell oy ox) => //. by move => eq; move: (proj2 h); rewrite eq. by move/(all_der_p5 oi) => [/(oltNge h)]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)