proposition: Lemma Zmullp_cons: forall a l, Zmullp (List.cons a l) = ((Ppow (fst a) (snd a)) * (Zmullp l))%positive.
proof: Proof. intros a l. assert (F1:= Pmult_assoc). assert (F2:= Pmult_comm). unfold Zmullp. simpl. rewrite F2; simpl Pmult. generalize (Ppow (fst a) (snd a)). elim l; simpl. - intros p; rewrite F2; auto. - intros a1 l1 Hrec p; rewrite Hrec. symmetry; rewrite Hrec. symmetry; rewrite F1. rewrite (F2 p); rewrite (fun x => (F2 x 1%positive)); auto. Qed.
imports: Ring Field_tac Ring_tac Eqdep_dec ZArith ZCAux Ppow GZnZ EGroup SMain Zmod