proposition: Lemma append_ok : forall x l r `{Ok l, Ok r}, lt_tree x l -> gt_tree x r -> Ok (append l r).
proof: Proof. append_tac l r. - trivial. - trivial. - intros; inv. assert (IH : Ok (append lr rl)) by (apply IHlr; eauto). clear IHlr. assert (X.lt lx rx) by (transitivity x; eauto). assert (G : gt_tree lx (append lr rl)). { intros w. autorew. destruct 1; [|transitivity x]; eauto. } assert (L : lt_tree rx (append lr rl)). { intros w. autorew. destruct 1; [transitivity x|]; eauto. } revert IH G L; case append_rr_match; intros; ok. - intros; ok. intros w; autorew; destruct 1; eauto. - intros; ok. intros w; autorew; destruct 1; eauto. - intros; inv. assert (IH : Ok (append lr rl)) by (apply IHlr; eauto). clear IHlr. assert (X.lt lx rx) by (transitivity x; eauto). assert (G : gt_tree lx (append lr rl)). { intros w. autorew. destruct 1; [|transitivity x]; eauto. } assert (L : lt_tree rx (append lr rl)). { intros w. autorew. destruct 1; [transitivity x|]; eauto. } revert IH G L; case append_bb_match; intros; ok. apply lbalS_ok; ok. Qed.
imports: Bool List BinPos Pnat Setoid SetoidList PeanoNat