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