proposition: Lemma subzn (m n : nat) : (n <= m)%N -> m%:Z - n%:Z = (m - n)%N.
proof: Proof. elim: n=> //= [|n ihn] hmn; first by rewrite subr0 subn0. rewrite subnS -addn1 !PoszD opprD addrA ihn 1?ltnW //. by rewrite intZmod.predn_int // subn_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)