proposition: Lemma Sba_jK: cancel Sba_j Sba_i.
proof: Proof. move => x. case xnz: (x == 0); first by rewrite /Sba_i/Sba_j (eqP xnz) invr0. have eq0: x = 1 - (1 - x) by rewrite opprB addrCA subrr addr0. rewrite Sba_j_prop ? xnz //. case h:(1 - x == 0); first by rewrite {3} eq0 (eqP h) /Sba_i invr0 mulr0. have h':1 - x != 0 by rewrite h. rewrite Sba_i_prop. rewrite (addf_div1 _ h') {2} (addrC 1). by rewrite addrA subrr add0r - mulf_div divr1 divff ?mulr1 // invr_eq0 . 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)