proposition: Lemma snumden_gt0 x: 0 < x -> (snumden x) != 0%N.
proof: Proof. move => xp; apply /negP => h. move: (snumden_pos (Order.POrderTheory.ltW xp)); rewrite (eqP h) /snumden' => eq1. move:xp (denq_gt0 x); rewrite - numq_gt0 ! gtz0_ge1 => sa sb. by move: (lerD sa sb); rewrite eq1. 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)