proposition: Lemma all_der_p11 x i j : ordinalp x -> i <=o j -> g x i <=o g x j.
proof: Proof. move => ox ij. move: (ij) => [oi oj _]. apply/(all_der_p10' ox ox oi oj); split => //. + move => lij. exact: (osi_gex (proj1 (all_der_p6 oj)) ox). + move => _; fprops. + by move => /(oleNgt ij). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)