proposition: Lemma Zlcm_gen_spec : forall l x, In x l -> Zdivides x (Zlcm_gen l).
proof: Proof. induction l. intros x Hin; destruct Hin. intros x Hin; destruct Hin. rewrite <- H; clear H. apply Zlcm_specl. fold (In x l) in H. simpl. apply (Zdivides_trans _ _ _ (IHl _ H)). apply Zlcm_specr. Qed.
imports: CRings Zring