proposition: Lemma addSpp p : xI p = (p + p).+1%N :> nat.
proof: Proof. by rewrite /= NatTrec.trecE addnn. 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