proposition: Lemma Zgcdn_is_gcd n a b : (Zgcd_bound a <= n)%nat -> Zis_gcd a b (Zgcdn n a b).
proof: Proof. destruct a. - simpl; intros. destruct n; [ lia | ]. simpl; generalize (Zis_gcd_0_abs b); intuition. - apply Zgcdn_is_gcd_pos. - rewrite <- Zgcd_bound_opp, <- Zgcdn_opp. intros. apply Zis_gcd_minus, Zis_gcd_sym. simpl Z.opp. now apply Zgcdn_is_gcd_pos. Qed.
imports: ZArith_base ZArithRing Zdiv Znumtheory Lia