proposition: Lemma id_continuoius: ocontinuous id.
proof: Proof. move => x /limit_ordinal_P [xp xl]. split; first by exists \0o => // i _ /proj1. by move => y lyx; exists (osucc y); [ apply: xl | move => i /oleSltP]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)