proposition: Lemma Zlcm_specl : forall a b : Z_as_CRing, Zdivides a (Zlcm a b).
proof: Proof. intros a b. unfold Zlcm. case (Z.eq_dec (Zgcd a b) ([0]:Z_as_CRing)). intro H; rewrite H; simpl. rewrite Zdiv_0_r. apply Zdivides_zero_rht. intro H; rewrite -> (Zgcd_div_mult_rht a b) at 1; [|assumption]. simpl. rewrite Zmult_assoc. rewrite Z_div_mult_full; [|assumption]. apply Zdivides_mult_rht. Qed.
imports: CRings Zring