Rings/Z: short proof of issemigrouppreserving_mult_rng_int_mult

theories/Algebra/Rings/Z.v

@@ -51,23 +51,8 @@ Global Instance issemigrouppreserving_mult_rng_int_mult (R : Ring)
 Proof.
   intros x y.
   cbn; unfold sg_op.
-  induction x as [|x|x].
-  - simpl.
-    by rhs nrapply rng_mult_zero_l.
-  - rewrite int_mul_succ_l.
-    rewrite grp_pow_add.
-    rewrite grp_pow_succ.
-    rhs nrapply rng_dist_r.
-    rewrite rng_mult_one_l.
-    f_ap.
-  - rewrite int_mul_pred_l.
-    rewrite grp_pow_add.
-    rewrite grp_pow_pred.
-    rhs nrapply rng_dist_r.
-    rewrite IHx.
-    f_ap.
-    lhs rapply (grp_homo_inv (grp_pow_homo 1)).
-    symmetry; apply rng_mult_negate.
+  lhs nrapply grp_pow_int_mul.
+  nrapply rng_int_mult_dist_l.
 Defined.
 
 (** [rng_int_mult R 1] is a ring homomorphism *)