proposition: Lemma OS_Szeta n: natp n -> ordinalp (Szeta n).
proof: Proof. move:n;apply: Nat_induction. rewrite Szeta_0; fprops. move => n nb Hrec; rewrite (Szeta_2 nb); apply:OS_Sphi; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)