proposition: Theorem zpmult_assoc: forall p q r, (zpmult p (zpmult q r)) = (zpmult (zpmult p q) r).
proof: Proof. assert (U: 0 < m); auto with zarith. intros p q r; unfold zpmult. generalize (pmult_assoc p q r). case (pmult p q); intros x1 x2. case (pmult q r); intros y1 y2. case p; case r; unfold pmult. intros z1 z2 t1 t2 H. match goal with H: (?X, ?Y) = (?Z, ?T) |- _ => assert (H1: X = Z); assert (H2: Y = T); try (injection H; simpl; auto; fail); clear H end. eq_tac. generalize (f_equal (fun x => x mod m) H1). repeat rewrite <- Zmult_assoc. repeat (rewrite (fun x => Zplus_mod (t1 * x))); auto. repeat (rewrite (fun x => Zplus_mod (x1 * x))); auto. repeat (rewrite (fun x => Zplus_mod (x1 mod m * x))); auto. repeat (rewrite (Zmult_mod t1)); auto. repeat (rewrite (Zmult_mod x1)); auto. repeat (rewrite (Zmult_mod base)); auto. repeat (rewrite (Zmult_mod t2)); auto. repeat (rewrite (Zmult_mod x2)); auto. repeat (rewrite (Zmult_mod (t2 mod m))); auto. repeat (rewrite (Zmult_mod (x1 mod m))); auto. repeat (rewrite (Zmult_mod (x2 mod m))); auto. repeat (rewrite Zmod_mod); auto. generalize (f_equal (fun x => x mod m) H2). repeat (rewrite (fun x => Zplus_mod (t1 * x))); auto. repeat (rewrite (fun x => Zplus_mod (x1 * x))); auto. repeat (rewrite (fun x => Zplus_mod (x1 mod m * x))); auto. repeat (rewrite (Zmult_mod t1)); auto. repeat (rewrite (Zmult_mod x1)); auto. repeat (rewrite (Zmult_mod t2)); auto. repeat (rewrite (Zmult_mod x2)); auto. repeat (rewrite (Zmult_mod (t2 mod m))); auto. repeat (rewrite (Zmult_mod (x1 mod m))); auto. repeat (rewrite (Zmult_mod (x2 mod m))); auto. repeat (rewrite Zmod_mod); auto. Qed.
imports: ZArith Znumtheory Tactic Wf_nat ListAux UList FGroup EGroup IGroup