proposition: Theorem cover_number_of_nodes : forall t l, cover l t -> number_of_nodes t = fold_left (fun x y => x + number_of_nodes y) l 0 + pred (length l).
proof: Proof. intros t l H; elim H; clear H t l; simpl in |- *; auto. intros l1 l2 t1 t2 t3 H H0 H1. apply trans_equal with (1 := H1). rewrite fold_left_permutation with (2 := H); simpl in |- *; auto. rewrite Permutation_length with (1 := H); simpl in |- *; auto. rewrite fold_left_init with (h := S); simpl in |- *; auto. intros a b1 b2; repeat rewrite <- Nat.add_assoc. apply f_equal2 with (f := plus); auto; apply Nat.add_comm. Qed.
imports: Coq(Sorting.Permutation ArithRing)