proposition: Lemma clt_omegaP x: x <c omega0 <-> natp x.
proof: Proof. split => h; first by move: (oclt h) => /olt_omegaP. by apply: oclt3; [fprops| apply: CS_omega | apply /olt_omegaP]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)