Implement copy modulo lock

[CohenCyril]

In spectral.v:

TODO: feature request
implement copy modulo lock

Lemma dotmx_bilinear n : isBilinear _ _ _ _ *%R (conjC \; *%R) (@dotmx C n).
Proof.
rewrite unlock; constructor => /= ?.
- exact: linearBl.
- exact: linearBr.
- exact: linearZl_LR.
- exact: linearZr_LR.
Qed.
HB.instance Definition _ n := dotmx_bilinear n.
**)

HB.instance Definition _ n := Bilinear.copy (@dotmx C n) (@dotmx C n).

cf

Originally posted by @proux01 in math-comp/math-comp#1519 (comment)