fact: Definition gcd a b := match a,b with | 0, _ => abs b | _, 0 => abs a | pos a, pos b => pos (Pos.gcd a b) | pos a, neg b => pos (Pos.gcd a b) | neg a, pos b => pos (Pos.gcd a b) | neg a, neg b => pos (Pos.gcd a b) end.
imports: BinNums BinPos BinNat