Coq 8.20, rm infra.v, minor fixes

[affeldt-aist]

This PR:

• removes the file infra.v (whose purpose was essentially to equip
  Z from the stdlib with the MathComp structures -> use ssrZ.v instead)
• update the opam file to support Coq 8.20
• other minor fixes so that make -j3 compiles up-to general_position.v
  that I am not sure is a file that actually ought to compile

[ybertot]

We need to change CI to use coq-8.20 and mathcomp2.3.0, if possible.

[affeldt-aist]

Let me try to add them.

[ybertot]

The new error message states that the build of infotheo is breaking. @affeldt-aist I need your help for this, but there is no hurry.

[affeldt-aist]

We have released recent versions of infotheo and I PRed a fix for an older version. This should fix the problem but we need to wait a bit for opam to be updated.

[affeldt-aist]

The second CI error (with Coq 8.20) is:

  - File "./theories/general_position.v", line 159, characters 12-57:
  - Error:
  - In environment
  - R : realFieldType
  - common_general_position_invariant :
  -   edge -> edge -> seq edge -> scan_state -> seq event -> Type
  - bottom : edge
  - top : edge
  - edge_set : seq edge
  - s : scan_state
  - events : seq event
  - The term "common_invariant bottom top edge_set s events" has type
  - "seq event -> seq event -> Prop" which should be Set, Prop or Type.

and indeed I have the same error on my laptop
(commit b857457).

[ybertot]

I know I corrected that file, that is why I believed I had pushed a correct version, but now I can't find my corrected version anymore. This is pain because I had a difficult modification of an inductive proof to perform, and I can't remember the exact trick. I will have to think again.

Yves

[ybertot]

This PR is now ready for squashing and merging. The problem with coq-8.19 has been studied and a solution is proposed in https://github.com/ybertot/trajectories/tree/lra_patch_for_coq_8.19 , but cannot be merged here because it adds workarounds that should not be kept for the long term.