proposition: Lemma treeify_cont_rb f g size1 size2 size d : treeify_rb_invariant size1 d f -> treeify_rb_invariant size2 d g -> size = S (size1 + size2) -> treeify_rb_invariant size (S d) (treeify_cont f g).
proof: Proof. intros Hf Hg H acc Hacc. unfold treeify_cont. specialize (Hf acc). destruct (f acc) as (l, acc1). simpl in *. destruct Hf as (Hf1, Hf2). { subst. eauto with arith. } destruct acc1 as [|(x,e) acc2]; simpl in *. - exfalso. revert Hacc. apply Nat.lt_nge. rewrite H, <- Hf2. auto with arith. - specialize (Hg acc2). destruct (g acc2) as (r, acc3). simpl in *. destruct Hg as (Hg1, Hg2). { revert Hacc. rewrite H, <- Hf2, Nat.add_succ_r, <- Nat.succ_le_mono. apply Nat.add_le_mono_l. } split; autom. now rewrite H, <- Hf2, <- Hg2, Nat.add_succ_r, Nat.add_assoc. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)