proposition: Lemma Zdiv_gcd_zero : forall a b, b / Z.gcd a b = 0 -> b <> 0 -> Z.gcd a b = 0.
proof: Proof. intros. generalize (Zgcd_is_gcd a b); destruct 1. destruct H2 as (k,Hk). generalize H; rewrite Hk at 1. destruct (Z.eq_dec (Z.gcd a b) 0) as [H'|H']; auto. rewrite Z_div_mult_full; auto. intros; subst k; simpl in *; subst b; elim H0; auto. Qed.
imports: ArithRing ZArith Znumtheory Zpow_facts Lia