proposition: Lemma Zlcm_spec : forall a b c : Z_as_CRing, Zdivides a c -> Zdivides b c -> Zdivides (Zlcm a b) c.
proof: Proof. intros a b c Hac Hbc; unfold Zlcm; simpl. case (Z.eq_dec (Zgcd a b) ([0]:Z_as_CRing)). intro H; rewrite H; simpl. destruct (Zgcd_zero _ _ H). rewrite H0 in Hac; clear H H0 H1. rewrite Zdiv_0_r; assumption. case (Z.eq_dec c ([0]:Z_as_CRing)). intro Hc; rewrite Hc. intro Hap; apply Zdivides_zero_rht. intros Hc Hap. apply Zdivides_abs_intro_rht. rewrite <- (Zmult_1_r (Z.abs c)). rewrite <- (Zgcd_div_gcd_1 a b); [|assumption]. rewrite Zgcd_lin. apply Zdiv_gcd_elim. cut (a * b / Zgcd a b = b * (a / Zgcd a b))%Z. intro H; rewrite H; clear H. apply Zdivides_mult_cancel_rht. assumption. rewrite Zmult_comm. apply (Zmult_reg_r _ _ (Zgcd a b) Hap). rewrite <- Zmult_assoc. rewrite <- (Zgcd_div_mult_lft _ _ Hap). rewrite Zmult_comm. rewrite <- (Z_div_exact_full_2 _ _ Hap). reflexivity. apply Zmod0_Zdivides. apply Hap. apply Zdivides_mult_elim_lft. apply Zgcd_is_divisor_lft. cut (a * b / Zgcd a b = a * (b / Zgcd a b))%Z. intro H; rewrite H; clear H. apply Zdivides_mult_cancel_rht. assumption. apply (Zmult_reg_r _ _ (Zgcd a b) Hap). rewrite <- Zmult_assoc. rewrite <- (Zgcd_div_mult_rht _ _ Hap). rewrite Zmult_comm. rewrite <- (Z_div_exact_full_2 _ _ Hap). reflexivity. apply Zmod0_Zdivides. apply Hap. apply Zdivides_mult_elim_lft. apply Zgcd_is_divisor_rht. Qed.
imports: CRings Zring