Avoid use of `solve_proper`.

Due to Coq bug #10480 or #10474 it actually used `Morphisms.solve_proper`
instead of the version of std++. The version in std++ can inherently
not solve this, so I changed it into a manual proof.
8 jobs for master in 9 minutes and 56 seconds (queued for 2 seconds)
Status Job ID Name Coverage
  Build
passed #41186
fp
build-coq.8.10.dev

00:08:03

passed #41192
fp
build-coq.8.7.2

00:02:54

passed #41191
fp-timing
build-coq.8.8.0

00:02:49

passed #41190
fp
build-coq.8.8.1

00:02:59

passed #41189
fp
build-coq.8.8.2

00:03:12

passed #41188
fp-timing
build-coq.8.9.0

00:03:32

passed #41187
fp
build-coq.8.9.1

00:03:56

passed #41185
fp
build-coq.dev

00:09:56