proposition: Lemma map_induction_max : forall P : t elt -> Type, (forall m, Empty m -> P m) -> (forall m m', P m -> forall x e, Above x m -> Add x e m m' -> P m') -> forall m, P m.
proof: Proof. intros; remember (cardinal m) as n; revert m Heqn; induction n; intros. - apply X; apply cardinal_inv_1; auto. - case_eq (max_elt m); intros. + destruct p. assert (Add k e (remove k m) m). * red; intros. rewrite add_o; rewrite remove_o; destruct (eq_dec k y); eauto. apply find_1; apply MapsTo_1 with k; auto. apply max_elt_MapsTo; auto. * apply X0 with (remove k m) k e; auto with map. -- apply IHn. assert (S n = S (cardinal (remove k m))). ++ rewrite Heqn. eapply cardinal_2; eauto with map ordered_type. ++ inversion H1; auto. -- eapply max_elt_Above; eauto. + apply X; apply max_elt_Empty; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface