to avoid a universe inconsistency with ring

[affeldt-aist]

Motivation for this change

It is possible that MathComp-Analysis 1.3.0 is not compatible with the ring tactics
in the sense that From mathcomp Require Import ring. triggers a universe inconsistency.
(Just try to import ring after anything that requires wochoice.)
That is not the first time that wochoice.v causes such a bug (#1198 (comment)).
It happens that avoiding the in3W lemma provides a way to void the problem.
(Tested on the prob_lang branches that rely a lot of ring, field, and lra.)
Hence this PR that I think should be merged asap and provided in MathComp-Analysis 1.4.0 asap.

Checklist

- [ ] added corresponding entries in CHANGELOG_UNRELEASED.md

- [ ] added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[affeldt-aist]

As feared:

affeldt-aist/monae#141