proposition: Theorem greater_values_sum : forall t:ntree Z, (forall x:Z, occurs Z x t -> 1 <= x)-> count Z t <= n_sum_values t.
proof: Proof. intros t; elim t using ntree_ind2 with (P0 := fun l:nforest Z => (forall x:Z, occurs_forest Z x l -> 1 <= x)-> count_list Z l <= n_sum_values_l l). - intros z l Hl Hocc; lazy beta iota delta -[Zplus Z.le]; fold count_list n_sum_values_l; auto with *. - auto with zarith. - intros t1 Hrec1 tl Hrec2 Hocc; lazy beta iota delta -[Zplus Z.le]; fold count count_list n_sum_values n_sum_values_l. apply Zplus_le_compat. apply Hrec1; intros; apply Hocc; apply occurs_head; auto. apply Hrec2; intros; apply Hocc; apply occurs_tail; auto. Qed.
imports: ZArith List Arith Zwf Relations Inverse_Image