fact: Fixpoint Zgcdn (n:nat) : Z -> Z -> Z := fun a b => match n with | O => 1 | S n => match a with | Z0 => Z.abs b | Zpos _ => Zgcdn n (Z.modulo b a) a | Zneg a => Zgcdn n (Z.modulo b (Zpos a)) (Zpos a) end end.
imports: ZArith_base ZArithRing Zdiv Znumtheory Lia