proposition: Lemma compare_cont_Cmp : forall s1 cont e2 l, (forall e, Cmp (cont e) l (flatten_e e)) -> Cmp (compare_cont s1 cont e2) (elements s1 ++ l) (flatten_e e2).
proof: Proof. induction s1 as [|c1 l1 Hl1 x1 r1 Hr1]; intros; auto. rewrite elements_node, <- app_assoc; simpl. apply Hl1; auto. clear e2. intros [|x2 r2 e2]. - simpl; auto. - apply compare_more_Cmp. rewrite <- cons_1; auto. Qed.
imports: Orders OrdersFacts MSetInterface PeanoNat