fact: Fixpoint compare x y := match x,y with | xH, xH => Eq | xH, _ => Lt | _, xH => Gt | xO a, xO b => compare a b | xI a, xI b => compare a b | xI a, xO b => Gt | xO a, xI b => Lt end.
imports: Coq(List) Coq(NArith)