proposition: Lemma compare_more_Cmp : forall x1 d1 cont x2 d2 r2 e2 l, Cmp (cont (R.cons r2 e2)) l (R.elements r2 ++ P.flatten_e e2) -> Cmp (compare_more x1 d1 cont (R.More x2 d2 r2 e2)) ((x1,d1)::l) (P.flatten_e (R.More x2 d2 r2 e2)).
proof: Proof. simpl; intros; destruct X.compare; simpl; try destruct D.compare; simpl; auto; P.MX.elim_comp; auto. Qed.
imports: FunInd FMapInterface FMapList ZArith Int