fact: Definition Zgcd_bound (a:Z) := match a with | Z0 => S O | Zpos p => let n := Pos.size_nat p in (n+n)%nat | Zneg p => let n := Pos.size_nat p in (n+n)%nat end.
imports: ZArith_base ZArithRing Zdiv Znumtheory Lia