proposition: Lemma until_mapmult_exp : forall (a : Z) (n : nat), zproduct (mapmult a (until n)) = (Exp a n * zproduct (until n))%Z.
proof: Proof. simple induction n. simpl in |- *. reflexivity. intros m IH. replace (mapmult a (until (S m))) with (Cons Z (a * Z_of_nat (S m))%Z (mapmult a (until m))). rewrite exp_S. replace (zproduct (Cons Z (a * Z_of_nat (S m))%Z (mapmult a (until m)))) with (a * Z_of_nat (S m) * zproduct (mapmult a (until m)))%Z. rewrite IH. rewrite Zmult_assoc_reverse. rewrite (Zmult_assoc (Z_of_nat (S m)) (Exp a m)). rewrite (Zmult_comm (Z_of_nat (S m))). rewrite Zmult_assoc. rewrite Zmult_assoc. replace (zproduct (until (S m))) with (Z_of_nat (S m) * zproduct (until m))%Z. rewrite Zmult_assoc. reflexivity. reflexivity. reflexivity. reflexivity. Qed.
imports: Arith ZArith lemmas natZ dec list exp divides prime modulo modprime