proposition: Lemma to_rtermE (t : GRing.term R) : GRing.rterm t -> to_rterm t = t :> GRing.term _.
proof: Proof. elim: t=> //=; do ? [ by move=> u hu v hv /andP[ru rv]; rewrite hu ?hv | by move=> u hu *; rewrite hu]. 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)