proposition: Theorem ordered_map_inv : forall (A B : Type) (order : A -> A -> Prop) (g : B -> A) (l : list B), ordered (fun x y => order (g x) (g y)) l -> ordered order (map g l).
proof: Proof. intros A B order g l; elim l; simpl in |- *; auto. intros a1 l1; case l1; simpl in |- *; auto. intros b l0 H H0; inversion H0; auto. Qed.
imports: Coq(Sorting.Permutation)