proposition: Lemma treeify_cont_spec f g size1 size2 size : treeify_invariant size1 f -> treeify_invariant size2 g -> size = S (size1 + size2) -> treeify_invariant size (treeify_cont f g).
proof: Proof. intros Hf Hg EQ acc LE. unfold treeify_cont. specialize (Hf acc). destruct (f acc) as (t1,acc1). destruct Hf as (Hf1,Hf2). { transitivity size; trivial. subst. rewrite <- Nat.add_succ_r. apply Nat.le_add_r. } destruct acc1 as [|x acc1]. { exfalso. revert LE. apply Nat.lt_nge. subst. rewrite app_nil_r, <- elements_cardinal. apply (Nat.succ_le_mono (cardinal t1)), Nat.le_add_r. } specialize (Hg acc1). destruct (g acc1) as (t2,acc2). destruct Hg as (Hg1,Hg2). { revert LE. subst. rewrite app_length, <- elements_cardinal. simpl. rewrite Nat.add_succ_r, <- Nat.succ_le_mono. apply Nat.add_le_mono_l. } rewrite elements_node, <- app_assoc. now subst. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat