[STATEMENT]
lemma test_mult_comm_var: "test p \<Longrightarrow> test q \<Longrightarrow> p \<cdot> q = q \<cdot> p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>test p; test q\<rbrakk> \<Longrightarrow> p \<cdot> q = q \<cdot> p
[PROOF STEP]
using n_mult_comm
[PROOF STATE]
proof (prove)
using this:
!?x \<cdot> !?y = !?y \<cdot> !?x

goal (1 subgoal):
 1. \<lbrakk>test p; test q\<rbrakk> \<Longrightarrow> p \<cdot> q = q \<cdot> p
[PROOF STEP]
by auto