proposition: Lemma isok_iff : forall s, Ok s <-> isok s = true.
proof: Proof. induction s as [|c l IHl y r IHr]; simpl. - intuition_in. - rewrite !andb_true_iff, <- IHl, <-IHr, <- ltb_tree_iff, <- gtb_tree_iff. intuition_in. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat