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). { apply max_elt_MapsTo, find_spec, add_id in H. unfold Add. symmetry. now rewrite add_remove_1. } 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_S; eauto with map. } inversion H1; auto. eapply max_elt_Above; eauto. apply X; apply max_elt_Empty; auto. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)