proposition: Lemma Zlcm_gen_spec2 : forall l x, (forall y, In y l -> Zdivides y x) -> Zdivides (Zlcm_gen l) x.
proof: Proof. induction l. intros; apply Zdivides_one. intros x H; apply Zlcm_spec. apply H; left; reflexivity. fold (Zlcm_gen l). apply IHl. intros y Hin; apply H. right; assumption. Qed.
imports: CRings Zring