proposition: Lemma wf_ex_elim : GRing.wf_QE_proj ex_elim.
proof: Proof. by move=> i bc /= rbc; apply: ex_elim_qf. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype generic_quotient bigop ssralg poly) mathcomp(polydiv matrix mxpoly countalg ring_quotient)