proposition: Lemma append_assoc_1 : forall (i j : positive), append i (xI j) = append (append i (xI xH)) j.
proof: Proof. induction i; intros; destruct j; simpl; try rewrite (IHi (xI j)); try rewrite (IHi (xO j)); try rewrite <- (IHi xH); auto. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface