Avoid repeating the same normalization in `field`

[pi8027]

As it can be seen in the following type, applying the Fcorrect lemma produces 5 subgoals:

Check Fcorrect
     : forall F (n : nat) (l : seq F) (lpe : seq (PExpr Z * PExpr Z)) (fe1 fe2 : FExpr Z),
       interp_PElist 0 1 +%R *%R (fun x y : F => x - y) -%R eq (fun n0 : Z => (int_of_Z n0)%:~R) N.to_nat
         (@GRing.exp _) l lpe ->
       (* three subterms shared below *)
       forall lmp : seq (Z * Mon * Pol Z),
       mk_monpol_list 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb (triv_div 0 1 Z.eqb) lpe = lmp ->
       forall nfe1 : Field_theory.linear Z,
       Fnorm 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb fe1 = nfe1 ->
       forall nfe2 : Field_theory.linear Z,
       Fnorm 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb fe2 = nfe2 ->
       (* normalization part *)
       Peq Z.eqb
         (norm_subst 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb (triv_div 0 1 Z.eqb) n lmp
            (PEmul (num nfe1) (denum nfe2)))
         (norm_subst 0 1 Z.add Z.mul Z.sub Z.opp Z.eqb (triv_div 0 1 Z.eqb) n lmp
            (PEmul (num nfe2) (denum nfe1))) = true ->
       (* conjunction of non-zero conditions *)
       PCond 0 1 +%R *%R (fun x y : F => x - y) -%R eq (fun n0 : Z => (int_of_Z n0)%:~R) N.to_nat
         (@GRing.exp _) l (condition nfe1 ++ condition nfe2)%list ->
       (* goal *)
       FEeval 0 1 +%R *%R (fun x y : F => x - y) -%R (fun x y : F => x / y) GRing.inv
         (fun n0 : Z => (int_of_Z n0)%:~R) N.to_nat (@GRing.exp _) l fe1 =
       FEeval 0 1 +%R *%R (fun x y : F => x - y) -%R (fun x y : F => x / y) GRing.inv
         (fun n0 : Z => (int_of_Z n0)%:~R) N.to_nat (@GRing.exp _) l fe2.

Before this PR, computation for the shared subterms was performed twice in the last two subgoals. https://github.com/math-comp/algebra-tactics/blob/350523a328b0b06829bea9e66edf2a1792295508/theories/ring.v#L453-L457

This PR fixes this performance issue, but what I do here (see the diff) looks really silly. I hope there is a smarter way to do the same thing... Maybe @amahboubi knows?

[pi8027]

One thing I don't understand here is that how the original field could avoid performing the same computation twice with this correctness lemma. I think invoking vm_compute; reflexivity for the first three subgoals does not really help here since readback (from VM values to Coq terms) and compilation (from Coq terms to VM code) can also be costly.

[pi8027]

FTR, this PR clearly makes compilation of apery faster. Maybe I should merge this anyway.

before:

make  789.30s user 11.23s system 99% cpu 13:21.28 total

after:

make  728.98s user 10.67s system 99% cpu 12:19.89 total