proposition: Lemma eval_rec_stable m n t b : (depth b <= m <= n)%N -> eval_rec n t b = eval_rec m t b.
proof: Proof. move=> /andP[bLm] /subnK<-; elim: (_ - _) {-2}m bLm => // {m}k IH m bLm. by rewrite addSnnS IH // ?eval_recS // (leq_trans bLm). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(all_algebra)