proposition: Lemma to_nat_gt0 p : 0 < Pos.to_nat p.
proof: Proof. by rewrite to_natE; elim: p => //= p; rewrite NatTrec.trecE double_gt0. Qed.
imports: ZArith Lia mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg ssrnum bigop ssrint) CoqEAL(hrel param refinements pos)