fact: Fixpoint compare (m m': t): comparison := match m,m' with | Leaf,_ => if is_empty m' then Eq else Lt | _,Leaf => if is_empty m then Eq else Gt | Node l o r,Node l' o' r' => lex (compare_bool o o') (lex (compare l l') (compare r r')) end.
imports: Bool PeanoNat BinPos Orders OrdersEx MSetInterface