proposition: Lemma Sba_iK: cancel Sba_i Sba_j.
proof: Proof. move => x. case xnz: (x == 0); first by rewrite /Sba_i/Sba_j (eqP xnz) invr0. have eq0: x = (1 + x) -1 by rewrite addrAC subrr add0r. rewrite (Sba_i_prop (negbT xnz)). case h:(1 + x == 0). by rewrite {3} eq0 (eqP h) /Sba_j invr0 mulr0 - div1r. rewrite Sba_j_prop. rewrite subf_div1 ?h //. by rewrite - addrA subrr addr0 - mulf_div divr1 divff ?mulr1 // invr_eq0 h. by rewrite mulf_eq0 xnz invr_eq0 h. 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)