fact: Fixpoint idx_compare i j := match i,j with | xH, xH => Eq | xH, _ => Lt | _, xH => Gt | xO i, xO j => idx_compare i j | xI i, xI j => idx_compare i j | xI _, xO _ => Gt | xO _, xI _ => Lt end.
imports: Coq(Arith NArith List RelationClasses)