proposition: Theorem height_pred_compute_code : forall (n : nat) (t : btree A), height_pred n (map (fun x => length (snd x) + n) (compute_code t)) (map (fun x => leaf (fst x)) (compute_code t)) t.
proof: Proof. intros n t; generalize n; elim t; clear t n; simpl in |- *; auto. intros b H b0 H0 n. repeat rewrite map_app. cut (forall (b : bool) l, map (fun x : A * list bool => length (snd x) + n) (map (fun v : A * list bool => let (a1, b1) := v in (a1, b :: b1)) l) = map (fun x : A * list bool => length (snd x) + S n) l); [ intros E1 | idtac ]. cut (forall b l, map (fun x : A * list bool => leaf (fst x)) (map (fun v : A * list bool => let (a1, b1) := v in (a1, b :: b1)) l) = map (fun x : A * list bool => leaf (fst x)) l); [ intros E2 | idtac ]. apply height_pred_node; repeat rewrite E1; repeat rewrite E2; auto. intros b1 l; elim l; simpl in |- *; auto. intros a; case a; simpl in |- *; auto. intros a0 l0 l1 H1; apply f_equal2 with (f := cons (A:=btree A)); auto. intros b1 l; elim l; simpl in |- *; auto. intros a; case a; simpl in |- *; auto. intros a0 l0 l1 H1; apply f_equal2 with (f := cons (A:=nat)); auto. Qed.
imports: Coq(ArithRing)