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. refine (Nat.le_trans _ _ _ _ Hacc). rewrite <- Nat.add_succ_r. apply Nat.le_add_r. } destruct acc1 as [|x acc2]; simpl in *. - exfalso. revert Hacc. apply Nat.lt_nge. rewrite H, <- Hf2. rewrite Nat.add_0_r. apply (Nat.succ_le_mono size1), Nat.le_add_r. - 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; auto. now rewrite H, <- Hf2, <- Hg2, Nat.add_succ_r, Nat.add_assoc. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat