proposition: Lemma Sba_m_pos_contra x: 0 < x -> {y:rat | (1 < y) && (Sba_m y == x) }.
proof: Proof. by move => h; exists (Sba_p x); rewrite Sba_pK eqxx andbT Sba_p_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)