proposition: Lemma zify_opp_subproof e1 : - rval e1 = (- zval e1)%:~R.
proof: Proof. by rewrite zifyRingE mulrNz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg ssrnum ssrint)