[STATEMENT]
lemma zero_vector_one_vector_vector:
  "zero_vector x \<Longrightarrow> one_vector x \<Longrightarrow> vector x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>zero_vector x; one_vector x\<rbrakk> \<Longrightarrow> vector x
[PROOF STEP]
by (metis one_vector_def vector_1 zero_vector_0)