Fixpoint product_of_leaves_acc (t : binary_tree_nat) (a : nat) : nat :=
  match t with
    | Leaf n => n * a
    | Node t1 t2 =>
      match a with
        | 0 => 0
        | n => product_of_leaves_acc t1 (product_of_leaves_acc t2 n)
      end
  end.