An exact proof term for the current goal is nat_p_SNo m Hm.

We will prove x ^ m * x ^ 0 = x ^ (m + 0).

rewrite the current goal using exp_SNo_nat_0 x Hx (from left to right).

rewrite the current goal using add_SNo_0R m Lm (from left to right).

An exact proof term for the current goal is mul_SNo_oneR (x ^ m) (SNo_exp_SNo_nat x Hx m Hm).

Let n be given.

Assume Hn: nat_p n.

Assume IHn: x ^ m * x ^ n = x ^ (m + n).

We will prove x ^ m * x ^ (ordsucc n) = x ^ (m + ordsucc n).

rewrite the current goal using exp_SNo_nat_S x Hx n Hn (from left to right).

We will prove x ^ m * (x * x ^ n) = x ^ (m + ordsucc n).

rewrite the current goal using add_nat_add_SNo m (nat_p_omega m Hm) (ordsucc n) (omega_ordsucc n (nat_p_omega n Hn)) (from right to left).

We will prove x ^ m * (x * x ^ n) = x ^ (add_nat m (ordsucc n)).

rewrite the current goal using add_nat_SR m n Hn (from left to right).

We will prove x ^ m * (x * x ^ n) = x ^ (ordsucc (add_nat m n)).

rewrite the current goal using exp_SNo_nat_S x Hx (add_nat m n) (add_nat_p m Hm n Hn) (from left to right).

We will prove x ^ m * (x * x ^ n) = x * x ^ (add_nat m n).

rewrite the current goal using add_nat_add_SNo m (nat_p_omega m Hm) n (nat_p_omega n Hn) (from left to right).

We will prove x ^ m * (x * x ^ n) = x * x ^ (m + n).

rewrite the current goal using IHn (from right to left).

We will prove x ^ m * (x * x ^ n) = x * (x ^ m * x ^ n).

rewrite the current goal using mul_SNo_assoc (x ^ m) x (x ^ n) (SNo_exp_SNo_nat x Hx m Hm) Hx (SNo_exp_SNo_nat x Hx n Hn) (from left to right).

We will prove (x ^ m * x) * x ^ n = x * (x ^ m * x ^ n).

rewrite the current goal using mul_SNo_com (x ^ m) x (SNo_exp_SNo_nat x Hx m Hm) Hx (from left to right).

We will prove (x * x ^ m) * x ^ n = x * (x ^ m * x ^ n).

Use symmetry.

An exact proof term for the current goal is mul_SNo_assoc x (x ^ m) (x ^ n) Hx (SNo_exp_SNo_nat x Hx m Hm) (SNo_exp_SNo_nat x Hx n Hn).