proposition: Lemma Szeta_5 n m: natp n -> natp m -> n <c m -> Szeta n <o Szeta m.
proof: Proof. move => nN mN nm. have pa: forall k, natp k -> k <> \0c -> Szeta n <o Szeta (n +c k). apply: Nat_induction => //. move => k kN Hrec _; rewrite (csum_nS _ kN). have hh: Szeta (n +c k) <o Szeta (csucc (n +c k)). apply:Szeta_4; fprops. case (equal_or_not k \0c) => kz. move: hh; rewrite {1} kz csum0r //; fprops. exact: (ole_ltT (proj1 (Hrec kz)) hh). rewrite - (cdiff_pr (proj1 nm)). apply: pa; [ by apply:NS_diff | exact: (cdiff_nz nm) ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)