Long Qed in `examples/std/int_to_Zp.v`

[t6s]

The last Qed in file examples/std/int_to_Zp.v (for IntRedModZp) takes many seconds.
The proof term is not large:

(fun Hyp : forall m n : 'Z_p, m = n * n -> m = n =>
 comap
   (Param01_forall int Zp Rp_weakened_to_2a0
      (fun m : int => forall n : int, m = int_mul n n -> eqmodp m n)
      (fun m' : Zp => forall n' : Zp, m' = Zp_mul n' n' -> eq_Zmodp m' n')
      (fun (m : int) (m' : Zp) (mR : Param2a0.R int Zp Rp_weakened_to_2a0 m m') =>
       Param01_forall int Zp Rp_weakened_to_2a0 (fun n : int => m = int_mul n n -> eqmodp m n)
         (fun n' : Zp => m' = Zp_mul n' n' -> eq_Zmodp m' n')
         (fun (n : int) (n' : Zp) (nR : Param2a0.R int Zp Rp_weakened_to_2a0 n n') =>
          Param01_arrow (m = int_mul n n) (m' = Zp_mul n' n')
            (Param10_paths int Zp Rp_weakened_to_2b0 m m' mR (int_mul n n) 
               (Zp_mul n' n') (Rmul n n' nR n n' nR))
            (eqmodp m n) (eq_Zmodp m' n') (Reqmodp01 m m' mR n n' nR))))
   ((Hyp : forall m' n' : Zp, m' = Zp_mul n' n' -> eq_Zmodp m' n')
    :
    forall m' n' : Zp, m' = Zp_mul n' n' -> eq_Zmodp m' n'))