proposition: Lemma Zmull_div: forall a l, List.In a l -> Zmull l = (Zmull l / a) * a :> Z.
proof: Proof. intros a l; generalize a; elim l; clear a l; auto. intros a H; inversion H. simpl List.In; intros a l Hrec b [H | H]; subst. rewrite Zmull_cons. repeat rewrite Zpos_mult_morphism. rewrite (Zmult_comm b). repeat rewrite Z_div_mult; auto. red; simpl; auto. repeat rewrite Zmull_cons. repeat rewrite Zpos_mult_morphism. rewrite (Hrec b); auto. rewrite Zmult_assoc. rewrite Z_div_mult; auto. red; simpl; auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod