proposition: Lemma gnode l o r i : find i (node l o r) = find i (Node l o r).
proof: Proof. destruct o,l,r; simpl; trivial. destruct i; simpl; now rewrite ?gleaf. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)