proposition: Lemma Sba_i_pos x: 0 < x -> 0 < Sba_i x < 1.
proof: Proof. move => h. have h1: 1 < 1 + x^-1 by apply: Sba_p_pos; rewrite invr_gt0. by move: (Order.POrderTheory.lt_trans ltr01 h1) => h2; rewrite invr_gt0 invf_lt1 h2. 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)