proposition: Lemma rcf_satP e f : reflect (holds e f) (rcf_sat e f).
proof: Proof. exact: (proj_satP wf_QE_wproj valid_QE_wproj). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(finfun path matrix) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp div ssrint) mathcomp(polyorder polyrcf interval polyXY) mathcomp(qe_rcf_th ordered_qelim mxtens)