proposition: Theorem ggcd_opp a b : ggcd (-a) b = (let '(g,(aa,bb)) := ggcd a b in (g,(-aa,bb))).
proof: Proof. destruct a as [|a|a], b as [|b|b]; unfold ggcd, opp; auto; destruct (Pos.ggcd a b) as (g,(aa,bb)); auto. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass