proposition: Lemma compare_Cmp : forall m1 m2, Cmp (compare_aux (Raw.cons m1 (Raw.End _), Raw.cons m2 (Raw.End _))) (Raw.elements m1) (Raw.elements m2).
proof: Proof. intros. assert (H1:=cons_1 m1 (Raw.End _)). assert (H2:=cons_1 m2 (Raw.End _)). simpl in *; rewrite app_nil_r in *; rewrite <-H1,<-H2. apply (@compare_aux_Cmp (Raw.cons m1 (Raw.End _), Raw.cons m2 (Raw.End _))). Qed.
imports: FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia