README: new install instructions

Author: YaelDillies

README.md

@@ -70,25 +70,16 @@ The following topics have been upstreamed to mathlib and no longer live in LeanC
 * The Erdős-Ginzburg-Ziv theorem
 * Chevalley's theorem about constructible sets with and without a complexity bound
 
-## Interacting with the project
-
-### Getting the project
+## Getting the project
 
 To build the Lean files of this project, you need to have a working version of Lean.
-See [the installation instructions](https://leanprover-community.github.io/get_started.html) (under Regular install).
-Alternatively, click on the button below to open a Gitpod workspace containing the project.
+See [the installation instructions](https://lean-lang.org/install/).
+Alternatively, click on the button below to open an Ona workspace containing the project.
 
-[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/#https://github.com/YaelDillies/apap)
+[![Open in Gitpod](https://gitpod.io/button/open-in-gitpod.svg)](https://gitpod.io/#https://github.com/YaelDillies/cam-combi)
 
 In either case, run `lake exe cache get` and then `lake build` to build the project.
 
-### Browsing the project
-
-With the project opened in VScode, you are all set to start exploring the code. There are two pieces of functionality that help a lot when browsing through Lean code:
-
-* "Go to definition": If you right-click on a name of a definition or lemma (such as `IsBinomialRandomGraph`), then you can choose "Go to definition" from the menu, and you will be taken to the relevant location in the source files. This also works by `Ctrl`-clicking on the name.
-* "Goal view": in the event that you would like to read a *proof*, you can step through the proof line-by-line, and see the internals of Lean's "brain" in the Goal window. If the Goal window is not open, you can open it by clicking on the forall icon in the top right hand corner.
-
 ### Contributing
 
 **This project is open to contribution**. You are in fact encouraged to have a look at the example sheet translations and try your hand at one of the problems. If you manage to prove one of them, please open a PR!