Lemma inf_height_labels : forall t : btree,
      height t <= nb_labels t.
Proof.
  intros.
  induction t.
  simpl.
  Search (_<=_).
  apply Nat.le_0_l.

  simpl.
  Search (S _ <= S _).
  apply le_n_S.
  Search ( max _ _ <= _).
  apply Nat.max_lub.
  Search ( _ <= _ + _).
  apply le_plus_trans.
  assumption.
  Search ( _ +_ ).
  rewrite Nat.add_comm.
  apply le_plus_trans.
  assumption.
Qed.