proposition: Lemma Zlcm_gen_nz : forall l, (forall x, In x l -> x [#] [0]) -> Zlcm_gen l [#] [0].
proof: Proof. induction l. intro; intro; discriminate. simpl. intros H1 H2; simpl. destruct (Zlcm_zero a (Zlcm_gen l) H2). apply (H1 a); [left; reflexivity|assumption]. destruct IHl; [|assumption]. intros; apply H1; right; assumption. Qed.
imports: CRings Zring