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