square with repeating ending xyxyxyxyxy

Author: thery

README.md

@@ -105,7 +105,15 @@ A note about factorions is available [here](https://inria.hal.science/hal-052656
 
 ## Building and installation instructions
 
-To build and install manually, do:
+The easiest way to install the latest released version of mathcomp-extra
+is via [OPAM](https://opam.ocaml.org/doc/Install.html):
+
+```shell
+opam repo add rocq-released https://rocq-prover.org/opam/released
+opam install coq-mathcomp-extra
+```
+
+To instead build and install manually, do:
 
 ``` shell
 git clone https://github.com/thery/mathcomp-extra.git

_CoqProject

@@ -37,3 +37,4 @@ cprime.v
 prime6.v
 liouville.v
 nicomachus.v
+repeatxy.v