proposition: Lemma Sn_gt1 (a b: int) (c := (a + b) - (a %% b)%Z *2) (A := a%:Q) (B := b%:Q) (C := c%:Q): 0 <= a -> 0 < b -> Sn ((A + B) / B) = B / (B + C).
proof: Proof. move => la lb; rewrite /Sn. have lt1 := (ltz_pmod a lb). have Bne: B != 0 by move: lb; rewrite lt0r intr_eq0 => /andP []. rewrite - [in RHS] invf_div (addrC B) - addf_div1 // -addf_div1 //. rewrite - addrA; congr ((1+ _) ^-1); rewrite opprD addrA -(addrK (A/B) (C/B)). congr (_ - (A/B)); rewrite - mulrDl - intrD (addrC 1) floor_succ floor_div //. rewrite doubleq - intrD addrACA - (intrD _ _ (-1)%Z) addrA addrK. rewrite /c /modz mulrBl opprB mulrAC (addrC a) addrACA -{3} (mul1r b) -mulrDl. by rewrite - mulz2 - addrA addrAC - mulz2 subrr addr0 intrM addrC -/B mulrK. 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)