proposition: Lemma find_1 : forall m (Hm:Sort m) x e, MapsTo x e m -> find x m = Some e.
proof: Proof. intros m Hm x e; generalize Hm; clear Hm; unfold MapsTo. functional induction (find x m);simpl; subst; try clear H_eq_1. inversion 2. inversion_clear 2. clear e1;compute in H0; destruct H0. apply lt_not_eq in H; auto. now contradict H. clear e1;generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute. intros. apply (lt_trans k') in _x; auto. apply lt_not_eq in _x. now contradict _x. clear e1;inversion_clear 2. compute in H0; destruct H0; intuition congruence. generalize (Sort_In_cons_1 Hm (InA_eqke_eqk H0)); compute. intros. apply lt_not_eq in H. now contradict H. clear e1; do 2 inversion_clear 1; auto. compute in H2; destruct H2. subst. apply lt_not_eq in _x. now contradict _x. Qed.
imports: SetoidList Bool OrderedType OrdersLists RelationPairs Orders RelationClasses