fact: Fixpoint SB_rec n x a b p := if n is n'.+1 then if (x < a + b) then SB_rec n' x a (a+b) (xO p) else if (a + b < x) then SB_rec n' x (a+b) b (xI p) else p else p.
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)