proposition: Theorem to_btree_smaller : forall t a, length (find_code A_eq_dec a (compute_code (to_btree t))) <= length (find_code A_eq_dec a (compute_pbcode t)).
proof: Proof. intros t; elim t; simpl in |- *; auto. intros p H a. apply Nat.le_trans with (1 := H a); auto. case (inpb_dec A_eq_dec (pbleaf a) p); intros H1. case inpb_compute_ex with (1 := H1). intros x Hx; rewrite in_find_map with (l := x); simpl in |- *; auto. rewrite not_in_find_map; simpl in |- *; auto. rewrite not_in_find_code; simpl in |- *; auto. intros p1; contradict H1; auto. apply in_pbcompute_inpb with (1 := H1). intros p1; contradict H1; auto. apply in_pbcompute_inpb with (1 := H1). intros p H a. apply Nat.le_trans with (1 := H a); auto. case (inpb_dec A_eq_dec (pbleaf a) p); intros H1. case inpb_compute_ex with (1 := H1). intros x Hx; rewrite in_find_map with (l := x); simpl in |- *; auto. rewrite not_in_find_map; simpl in |- *; auto. rewrite not_in_find_code; simpl in |- *; auto. intros p1; contradict H1; auto. apply in_pbcompute_inpb with (1 := H1). intros p1; contradict H1; auto. apply in_pbcompute_inpb with (1 := H1). intros p H p0 H0 a. simpl in |- *; repeat rewrite find_code_app; auto. case (inpb_dec A_eq_dec (pbleaf a) p); intros H1. case inpb_compute_ex with (1 := H1). intros x Hx; repeat rewrite in_find_map with (1 := Hx); simpl in |- *; auto with arith. case inb_compute_ex with (a := a) (p := to_btree p); auto. apply to_btree_inb; auto. intros x1 Hx1; repeat rewrite in_find_map with (1 := Hx1); simpl in |- *; auto with arith. rewrite not_in_find_map with (p := compute_code (to_btree p)); simpl in |- *; auto with arith. rewrite not_in_find_map with (p := compute_pbcode p); simpl in |- *; auto with arith. case (inpb_dec A_eq_dec (pbleaf a) p0); intros H2. case inpb_compute_ex with (1 := H2). intros x Hx; repeat rewrite in_find_map with (1 := Hx); simpl in |- *; auto with arith. case inb_compute_ex with (a := a) (p := to_btree p0); auto. apply to_btree_inb; auto. intros x1 Hx1; repeat rewrite in_find_map with (1 := Hx1); simpl in |- *; auto with arith. rewrite not_in_find_map with (p := compute_pbcode p0); simpl in |- *; auto with arith. rewrite not_in_find_map with (p := compute_code (to_btree p0)); simpl in |- *; auto with arith. intros l; contradict H2; apply to_btree_inpb; apply inCompute_inb with (1 := H2); auto. intros l; contradict H2; apply in_pbcompute_inpb with (1 := H2). intros l; contradict H1; apply in_pbcompute_inpb with (1 := H1). intros l; contradict H1; apply to_btree_inpb; apply inCompute_inb with (1 := H1); auto. Qed.