[STATEMENT]
lemma dim_row_of_one_mat_less_pow:
  assumes "gate m G1" and "gate n G2" and "i < dim_row (1\<^sub>m(dim_col G1 * dim_col G2))"
  shows "i < 2^(m+n)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. i < 2 ^ (m + n)
[PROOF STEP]
using assms gate_def
[PROOF STATE]
proof (prove)
using this:
gate m G1
gate n G2
i < dim_row (1\<^sub>m (dim_col G1 * dim_col G2))
gate ?n ?A \<equiv> dim_row ?A = 2 ^ ?n \<and> square_mat ?A \<and> unitary ?A

goal (1 subgoal):
 1. i < 2 ^ (m + n)
[PROOF STEP]
by (simp add: power_add)