proposition: Lemma set_induction_min : forall P : t -> Type, (forall s : t, Empty s -> P s) -> (forall s s', P s -> forall x, Below x s -> Add x s s' -> P s') -> forall s : t, P s.
proof: Proof. intros; remember (cardinal s) as n; revert s Heqn; induction n; intros; auto. case_eq (min_elt s); intros. - apply X0 with (remove e s) e; auto with set. + apply IHn. assert (S n = S (cardinal (remove e s))). { rewrite Heqn; apply cardinal_2 with e; auto with set relations. } inversion H0; auto. + red; intros. rewrite remove_iff in H0; destruct H0. generalize (@min_elt_spec2 s e y H H0); order. - assert (H0:=min_elt_spec3 H). rewrite cardinal_Empty in H0; auto; rewrite H0 in Heqn; inversion Heqn. Qed.
imports: MSetInterface PeanoNat DecidableTypeEx OrdersLists MSetFacts MSetDecide