proposition: Lemma lt0p : forall p : positive, 0 < p.
proof: Proof. by elim=> // p IHp /=; rewrite NatTrec.doubleE -addnn; exact:ltn_addl. Qed.
imports: ZArith Ncring Ncring_tac mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice fintype) mathcomp(div finfun bigop prime binomial ssralg finset fingroup finalg) mathcomp(perm zmodp matrix) ssralg_ring_tac