proposition: Lemma Szeta_4 k: natp k -> Szeta k <o Szeta (csucc k).
proof: Proof. move => kb; rewrite (Szeta_2 kb); move:(OS_Szeta kb) => ox. split; first exact:(Sphi_p9 ox). move => eq. case: (oleNgt (proj2 (Gamma0_p) _ ox (sym_eq eq)) (Szeta_3 kb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)