proposition: Lemma qf_simpl (f : fF) : (qf f -> GRing.qf_form f) * (qf f -> GRing.rformula f).
proof: Proof. by split=> /andP[]. 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)