proposition: Lemma rabstrX (i : nat) (t : tF) : rterm t -> rpoly (abstrX i t).
proof: Proof. elim: t; do ?[ by move=> * //=; do ?case: (_ == _)]. - move=> t irt s irs /=; case/andP=> rt rs. by apply: rsumpT; rewrite ?irt ?irs //. - by move=> t irt /= rt; rewrite rpoly_map_mul ?irt //. - by move=> t irt /= n rt; rewrite rpoly_map_mul ?irt //. - move=> t irt s irs /=; case/andP=> rt rs. by apply: rmulpT; rewrite ?irt ?irs //. - move=> t irt /= n rt; move: (irt rt) => {}rt; elim: n => [|n ihn] //=. exact: rmulpT. 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)