proposition: Theorem number_of_nodes_inb_le : forall t1 t2, inb t1 t2 -> number_of_nodes t1 <= number_of_nodes t2.
proof: Proof. intros t1 t2 H; elim H; clear H t1 t2; simpl in |- *; auto. intros t t1 t2 H H0; apply Nat.le_trans with (1 := H0); auto with arith. intros t t1 t2 H H0; apply Nat.le_trans with (1 := H0); auto with arith. Qed.
imports: Coq(ArithRing ListDec)