Let x be given.
Assume Hx.
Let m be given.
Assume Hm.
We prove the intermediate claim Lm: SNo m.
An exact proof term for the current goal is nat_p_SNo m Hm.
Apply nat_ind to the current goal.
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).
∎