proposition: Lemma olimit_succ f x l: ordinalp l -> (olimit f x (osucc l) <-> econst f x (osucc l)).
proof: Proof. move => ol. split; last by apply: olimit_econst; apply: OS_succ. move =>[ [y ya yb] etc]. move: (etc _ (oltS ol)) => [z za zb]. exists (omax y z); first by rewrite/omax/Gmax; Ytac h. move => i la lb. move: (omax_p1 (proj31_1 ya) (proj31_1 za)) => [lc ld]. apply: oleA; first exact: (yb _ (oleT lc la) lb). apply/oleSltP; exact (zb _ (oleT ld la) lb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)