proposition: Lemma osum_Mon1 f n i: natp n -> i <c n -> ord_below f n -> f i <=o osumf f n.
proof: Proof. move:n; apply: Nat_induction; first by move => /clt0. move => n nN Hrec /(cltSleP nN) /cle_eqVlt lin axs. move:(true_below_rec nN axs) => [axn ax1]. rewrite (osum_fS _ nN). case:lin; first by move ->; exact:(osum_Mle0 ax1 (OS_osumf nN axn)) => le1. move => lin; exact: (oleT (Hrec lin axn) (osum_M0le ax1 (OS_osumf nN axn))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)