proposition: Lemma combine_1 : forall m (Hm : sort (@ltk elt) m) m' (Hm' : sort (@ltk elt') m') (x:key), find x (combine m m') = at_least_one (find x m) (find x m').
proof: Proof. induction m. - intros. simpl. induction m'. + intros; simpl; auto. + simpl; destruct a. simpl; destruct (X.compare x t0); simpl; auto. inversion_clear Hm'; auto. - induction m'. + intros; destruct a; simpl. destruct (X.compare x t0) as [Hlt| |Hlt]; simpl; auto. inversion_clear Hm; clear H0 Hlt Hm' IHm t0. induction m; simpl; auto. inversion_clear H. destruct a. simpl; destruct (X.compare x t0); simpl; auto. + intros. destruct a as (k,e); destruct a0 as (k',e'); simpl. inversion Hm; inversion Hm'; subst. destruct (X.compare k k'); simpl; destruct (X.compare x k); elim_comp || destruct (X.compare x k'); simpl; auto. * rewrite IHm; auto; simpl; elim_comp; auto. * rewrite IHm; auto; simpl; elim_comp; auto. * rewrite IHm; auto; simpl; elim_comp; auto. * change (find x (combine ((k, e) :: m) m') = at_least_one None (find x m')). rewrite IHm'; auto. simpl find; elim_comp; auto. * change (find x (combine ((k, e) :: m) m') = Some (Some e, find x m')). rewrite IHm'; auto. simpl find; elim_comp; auto. * change (find x (combine ((k, e) :: m) m') = at_least_one (find x m) (find x m')). rewrite IHm'; auto. simpl find; elim_comp; auto. Qed.
imports: FMapInterface