proposition: Lemma zify_mul_subproof e1 e2 : rval e1 * rval e2 = (zval e1 * zval e2)%:~R.
proof: Proof. by rewrite 2!zifyRingE intrM. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg ssrnum ssrint)