proposition: Lemma SCF2_bis (a b: rat) : b != 0 -> 1/ (a + 1 / b) = b / (a * b + 1).
proof: Proof. by move => bz; rewrite !div1r addf_inv // invf_div. 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)