proposition: Lemma nat_of_pos_gtr0 p : (0 < Posz (nat_of_pos p))%R.
proof: Proof. by rewrite -[0%R]/(Posz 0) ltz_nat nat_of_pos_gt0. Qed.
imports: ZArith QArith Lia Bignums(BigQ) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat order) mathcomp(ssralg ssrnum ssrint rat div intdiv) CoqEAL.refinements(hrel refinements param binint)