fact: Fixpoint to_rterm (t : term R) (r : seq (term R)) (n : nat) {struct t} := match t with | t1^-1 => let: (t1', r1) := to_rterm t1 r n in ('X_(n + size r1), rcons r1 t1') | t1 + t2 => let: (t1', r1) := to_rterm t1 r n in let: (t2', r2) := to_rterm t2 r1 n in (t1' + t2', r2) | - t1 => let: (t1', r1) := to_rterm t1 r n in (- t1', r1) | t1 *+ m => let: (t1', r1) := to_rterm t1 r n in (t1' *+ m, r1) | t1 * t2 => let: (t1', r1) := to_rterm t1 r n in let: (t2', r2) := to_rterm t2 r1 n in (Mul t1' t2', r2) | t1 ^+ m => let: (t1', r1) := to_rterm t1 r n in (t1' ^+ m, r1) | _ => (t, r) end%T.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)