proposition: Lemma Sba_j_pos_contra x: 0 < x -> {y:rat | (0 < y <1) && (Sba_j y == x) }.
proof: Proof. move => h; exists (Sba_i x); rewrite Sba_iK eqxx andbT; exact:Sba_i_pos. 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)