proposition: Lemma to_rterm_id t r n : rterm t -> to_rterm t r n = (t, r).
proof: Proof. elim: t r n => //. - by move=> t1 IHt1 t2 IHt2 r n /= /andP[rt1 rt2]; rewrite {}IHt1 // IHt2. - by move=> t IHt r n /= rt; rewrite {}IHt. - by move=> t IHt r n m /= rt; rewrite {}IHt. - by move=> t1 IHt1 t2 IHt2 r n /= /andP[rt1 rt2]; rewrite {}IHt1 // IHt2. - by move=> t IHt r n m /= rt; rewrite {}IHt. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop prime binomial)