proposition: Lemma to_rform_rformula f : rformula (to_rform f).
proof: Proof. suffices [h1 h2 h3]: [/\ forall t1, rformula (eq0_rform t1), forall t1, rformula (lt0_rform t1) & forall t1, rformula (leq0_rform t1)]. by elim: f => //= => f1 ->. split=> t1. - rewrite /eq0_rform; move: (ub_var t1) => m. set tr := _ m. suffices: all (@rterm R) (tr.1 :: tr.2)%PAIR. case: tr => {}t1 r /= /andP[t1_r]. by elim: r m => [|t r IHr] m; rewrite /= ?andbT // => /andP[->]; apply: IHr. have: all (@rterm R) [::] 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. - rewrite /lt0_rform; move: (ub_var t1) => m; set tr := _ m. suffices: all (@rterm R) (tr.1 :: tr.2)%PAIR. case: tr => {}t1 r /= /andP[t1_r]. by elim: r m => [|t r IHr] m; rewrite /= ?andbT // => /andP[->]; apply: IHr. have: all (@rterm R) [::] 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. - rewrite /leq0_rform; move: (ub_var t1) => m; set tr := _ m. suffices: all (@rterm R) (tr.1 :: tr.2)%PAIR. case: tr => {}t1 r /= /andP[t1_r]. by elim: r m => [|t r IHr] m; rewrite /= ?andbT // => /andP[->]; apply: IHr. have: all (@rterm R) [::] 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.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div choice fintype) mathcomp(bigop order ssralg finset fingroup zmodp) mathcomp(poly ssrnum)