proposition: Lemma nat_of_pos_ne0 p: nat_of_pos p != 0.
proof: Proof. by move: (nat_of_binK (Npos p)) => /=; case: (nat_of_pos p). 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)