proposition: Lemma zify_exprn_subproof e1 n : rval e1 ^+ n = (zval e1 ^+ n)%:~R.
proof: Proof. by rewrite zifyRingE; elim: n => //= n; rewrite !exprS intrM => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg ssrnum ssrint)