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