proposition: Lemma combine_sorted : forall m (Hm : sort (@ltk elt) m) m' (Hm' : sort (@ltk elt') m'), sort (@ltk oee') (combine m m').
proof: Proof. induction m. - intros; clear Hm. simpl. apply map_sorted; auto. - induction m'. + intros; clear Hm'. destruct a. replace (combine ((t0, e) :: m) nil) with (map (fun e => (Some e,None (A:=elt'))) ((t0,e)::m)); auto. apply map_sorted; auto. + intros. simpl. destruct a as (k,e); destruct a0 as (k',e'). destruct (X.compare k k') as [Hlt|Heq|Hlt]. * inversion_clear Hm. constructor; auto. assert (lelistA (ltk (elt:=elt')) (k, e') ((k',e')::m')) by auto. exact (combine_lelistA _ H0 H1). * inversion_clear Hm; inversion_clear Hm'. constructor; auto. assert (lelistA (ltk (elt:=elt')) (k, e') m') by (apply Inf_eq with (k',e'); auto). exact (combine_lelistA _ H0 H3). * inversion_clear Hm; inversion_clear Hm'. constructor; auto. change (lelistA (ltk (elt:=oee')) (k', (None, Some e')) (combine ((k,e)::m) m')). assert (lelistA (ltk (elt:=elt)) (k', e) ((k,e)::m)) by auto. exact (combine_lelistA _ H3 H2). Qed.
imports: FMapInterface