fact: Definition compare x y := match x, y with | 0, 0 => Eq | 0, pos y' => Lt | 0, neg y' => Gt | pos x', 0 => Gt | pos x', pos y' => (x' ?= y')%positive | pos x', neg y' => Gt | neg x', 0 => Lt | neg x', pos y' => Lt | neg x', neg y' => CompOpp ((x' ?= y')%positive) end.
imports: BinNums BinPos BinNat