proposition: Lemma Zlcm_zero : forall p q, Zlcm p q [=] [0] -> p [=] [0] or q [=] [0].
proof: Proof. intros p q; unfold Zlcm; intro Heq. case (Z.eq_dec p ([0]:Z_as_CRing)). left; assumption. intro Happ; right. simpl in *. unfold ap_Z in Happ. apply (Zmult_integral_l _ _ Happ). rewrite Zmult_comm. revert Heq. assert (Zgcd p q <> 0%Z). intro H; destruct Happ; apply (Zgcd_zero _ _ H). rewrite -> (Zgcd_div_mult_lft p q) at 1; [|assumption]. rewrite (Zmult_comm (p / Zgcd p q)). rewrite <- Zmult_assoc. rewrite Zdiv_mult_cancel_lft; [|assumption]. intro Heq. rewrite (Zgcd_div_mult_lft p q); [|assumption]. rewrite <- Zmult_assoc, (Zmult_comm _ q), Zmult_assoc. rewrite Heq, Zmult_0_l; reflexivity. Qed.
imports: CRings Zring