proposition: Lemma Sba_m_snum x: 1 < x -> (snumden (Sba_m x) < snumden x)%N.
proof: Proof. suff: 1 <x -> snumden' (Sba_m x) < snumden' x. move => H x1; move: (H x1). rewrite (snumden_pos(Order.POrderTheory.ltW(Sba_m_pos x1))). by rewrite (snumden_pos(Order.POrderTheory.ltW (Order.POrderTheory.lt_trans ltr01 x1))). rewrite /Sba_m -subr_gt0 -{3} (subrK 1 x) -numq_gt0 /snumden /snumden'. case/ratP: (x-1) => n d cp n0. have H: coprime `|n + d.+1| d.+1. by rewrite - (gtz0_abs n0) - PoszD /= /coprime gcdnC gcdnDr gcdnC. rewrite (addrC _ 1) addf_div1 ?intr_eq0 //- intrD coprimeq_den //. by rewrite coprimeq_num // sgrEz /= gtr0_sgz // mul1r ltrDl normr_gt0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq choice fintype order bigop ssralg) mathcomp(div ssrnum ssrint rat prime path binomial) mathcomp(tuple finset) gaia(fibm)