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 build-coq.8.10.dev #41186
fp

00:08:03

passed build-coq.8.7.2 #41192
fp

00:02:54

passed build-coq.8.8.0 #41191
fp-timing

00:02:49

passed build-coq.8.8.1 #41190
fp

00:02:59

passed build-coq.8.8.2 #41189
fp

00:03:12

passed build-coq.8.9.0 #41188
fp-timing

00:03:32

passed build-coq.8.9.1 #41187
fp

00:03:56

passed build-coq.dev #41185
fp

00:09:56