proposition: Lemma Sn_gt0 x: 0 <= x -> 0 < Sn x.
proof: Proof. rewrite /Sn doubleq addrA (addrC (1 + _)) -addrA => h. rewrite invr_gt0 -(addr0 0); apply:ler_ltD;first by rewrite ler0z floor_ge0. by rewrite subr_gt0 addrC; case /andP:(floorp1 x) => [_]. 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)