proposition: Lemma addf_inv x y: y != 0 -> x + y^-1 = (x*y +1)/y.
proof: Proof. by move => h; rewrite mulrDl div1r mulfK. 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)