proposition: Lemma remove_min_gt_tree : forall l x r h `{Ok (Node h l x r)}, gt_tree (remove_min l x r)#2 (remove_min l x r)#1.
proof: Proof. intros l x r; functional induction (remove_min l x r); simpl; intros. - inv; auto. - assert (O : Ok (Node _x ll lx lr)) by (inv; auto). assert (L : lt_tree x (Node _x ll lx lr)) by (inv; auto). specialize IHp with (1:=O); rewrite e0 in IHp; simpl in IHp. intro y; rewrite bal_spec; intuition; specialize (L m); rewrite remove_min_spec, e0 in L; simpl in L; [setoid_replace y with x|inv]; eauto. Qed.
imports: FunInd MSetInterface MSetGenTree BinInt Int