proposition: Fact ra_exp_val n m : ⟦ra_exp⟧ (n##m##vec_nil) (power n m).
proof: Proof. unfold ra_exp. rewrite ra_iter_n_rel with (f := fun _ => 1) (g := fun v i => vec_head v*i). + simpl; induction n. * rewrite power_0; auto. * rewrite power_S; simpl; f_equal; auto. + apply ra_cst_n_val. + intros i v; vec split v with j; vec nil v; simpl. exists (j##i##vec_nil); split; auto. pos split; simpl; auto. Qed.
imports: Arith List Lia Undecidability.Shared.Libs.DLW(utils_tac utils_nat utils_list gcd crt sums finite pos vec) Undecidability.MuRec.Util(recalg recomp prim_min)