proposition: Lemma Zgcdn_pos : forall n a b, 0 <= Zgcdn n a b.
proof: Proof. intros n; induction n. - simpl; auto with zarith. - intros a; destruct a; simpl; intros; auto with zarith; auto. Qed.
imports: ZArith_base ZArithRing Zdiv Znumtheory Lia