proposition: Fact nat_of_posE : nat_of_pos =1 Pos.to_nat.
proof: Proof. move=> p; rewrite /Pos.to_nat -[LHS]muln1. elim: p 1 => /= [p IHp | p IHp |] n; rewrite -?IHp; lia. Qed.
imports: Coq(ZArith ZifyClasses ZifyInst ZifyBool) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop finset prime) mathcomp(order binomial)