proposition: Lemma nat_of_pos_gt0 p : (0 < nat_of_pos p)%N.
proof: Proof. by elim: p =>//= p IHp; rewrite NatTrec.doubleE double_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)