proposition: Lemma nat_of_posK p: pos_of_nat' (nat_of_pos p).-1 = p.
proof: Proof. have ni: injective Npos by move => a b; case. by apply: ni; 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)