proposition: Lemma to_rform_rformula f : rformula (to_rform f).
proof: Proof. suffices eq0_ring t1: rformula (eq0_rform t1) by elim: f => //= => f1 ->. rewrite /eq0_rform; move: (ub_var t1) => m; set tr := _ m. suffices: all rterm (tr.1 :: tr.2). case: tr => {}t1 r /= /andP[t1_r]. by elim: r m => [|t r IHr] m; rewrite /= ?andbT // => /andP[->]; apply: IHr. have: all rterm [::] by []. rewrite {}/tr; elim: t1 [::] => //=. - move=> t1 IHt1 t2 IHt2 r. move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r]. move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r]. by rewrite t1_r t2_r. - by move=> t1 IHt1 r /IHt1; case: to_rterm. - by move=> t1 IHt1 n r /IHt1; case: to_rterm. - move=> t1 IHt1 t2 IHt2 r. move/IHt1; case: to_rterm => {r IHt1}t1 r /= /andP[t1_r]. move/IHt2; case: to_rterm => {r IHt2}t2 r /= /andP[t2_r]. by rewrite t1_r t2_r. - move=> t1 IHt1 r. by move/IHt1; case: to_rterm => {r IHt1}t1 r /=; rewrite all_rcons. - by move=> t1 IHt1 n r /IHt1; case: to_rterm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)