proposition: Lemma olimit_unique f x a b: limit_ordinal x -> olimit f x a -> olimit f x b -> a = b.
proof: Proof. move => lx ha hb. move: (OS_olim ha) (OS_olim hb) => oa ob. move: ha hb => [[y ya yb] yc] [[z za zb] zc]. case: (oleT_ell oa ob) => // cab. move: (zc a cab) => [t ta tb]. move: (omax_p1 (proj31_1 ya) (proj31_1 ta)) =>[la lb]. have lc: omax y t <o x by rewrite /omax/Gmax; Ytac h. by move:(yb _ la lc) (oltNge (tb _ lb lc)). move: (yc b cab) => [t ta tb]. move: (omax_p1 (proj31_1 za) (proj31_1 ta)) =>[la lb]. have lc: omax z t <o x by rewrite /omax/Gmax; Ytac h. by move:(zb _ la lc) (oltNge (tb _ lb lc)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)