proposition: Lemma Szeta_3 n: natp n -> Szeta n <o Gamma_0.
proof: Proof. move: n; apply:Nat_induction. move: Gamma0_limit (olt_1omega) => /limit_ge_omega ha hb. rewrite Szeta_0; apply: olt_leT hb ha. move => n nb Hrec; rewrite (Szeta_2 nb). by rewrite -(proj1 (Gamma0_p)); move: (proj1 (Sphi_p5) _ _ Hrec). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)