[STATEMENT]
lemma zero_vector_5:
  "zero_vector x \<longleftrightarrow> x * top = x * bot"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. zero_vector x = (x * top = x * bot)
[PROOF STEP]
by (metis top_right_mult_increasing zero_vector_def zero_vector_left_zero)