[STATEMENT]
lemma fast_ppoint_mult_even [simp]:
  "n \<noteq> 0 \<Longrightarrow> n mod 2 = 0 \<Longrightarrow>
   fast_ppoint_mult m a n p = mpdouble m a (fast_ppoint_mult m a (n div 2) p)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>n \<noteq> 0; n mod 2 = 0\<rbrakk> \<Longrightarrow> fast_ppoint_mult m a n p = mpdouble m a (fast_ppoint_mult m a (n div 2) p)
[PROOF STEP]
by simp