proposition: Lemma combine_r_1 : forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m')(x:key), find x (combine_r m m') = at_least_right (find x m) (find x m').
proof: Proof. unfold combine_r. intros. case_eq (find x m'); intros. - simpl. apply find_1. + apply mapi_NoDup; auto. + destruct (mapi_1 (fun k e => (find k m, Some e)) (find_2 H)) as (y,(H0,H1)). rewrite (find_eq Hm (X.eq_sym H0)); auto. - simpl. case_eq (find x (mapi (fun k e' => (find k m, Some e')) m')); intros; auto. destruct (@mapi_2 _ _ m' x (fun k e' => (find k m, Some e'))). + exists p; apply find_2; auto. + rewrite (find_1 Hm' H1) in H; discriminate. Qed.
imports: FMapInterface