proposition: Lemma Sn_lt1 (a b: int) (A := a%:Q) (B := b%:Q): 0 <= a -> 0 < b -> Sn (A / (A + B)) = (A + B) / B.
proof: Proof. move => la lb; move: (ler_ltD la lb); rewrite addr0 => lab. have labq: 0 < (a + b)%:Q by rewrite ltr0z. have dnz: (a + b)%:Q != 0 by move: labq; rewrite lt0r => /andP []. have ha: 0 <= a%:Q / (a + b)%:Q < 1. rewrite divr_ge0 ?ler0z ? (ltrW lab)//= ?ltr_pdivrMr //. by rewrite mul1r ltr_int - {1} (addr0 a) ltrD2l. by move: lab; rewrite lt0r; move/andP => [la1 la2]. rewrite Sn_small - intrD // -(invf_div b%:~R) subf_div1 //. by rewrite - rmorphB /= {1} (addrC a) - addrA subrr addr0. 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)