fact: Fixpoint n_sum_values (t:ntree Z) : Z := match t with | nnode _ z l => z + n_sum_values_l l end with n_sum_values_l (l:nforest Z) : Z := match l with | nnil _ => 0 | ncons _ t tl => n_sum_values t + n_sum_values_l tl end.
imports: ZArith List Arith Zwf Relations Inverse_Image