proposition: Lemma Sba_i_prop x: x != 0 -> Sba_i x = x /(1 + x).
proof: Proof. by move => xnz; rewrite /Sba_i -(div1r x) addf_div1 // invf_div. 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)