proposition: Lemma addf_div1 x y: y != 0 -> 1 + x / y = (x+y) /y.
proof: Proof. move: (oner_neq0 F) => ha hb. by rewrite -(divff ha) addf_div // mul1r mulr1 addrC. 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)