Sergey Bozhko authored 3 years ago and Björn Brandenburg committed 3 years ago

I think that this experiment was not successful. These lemmas can be
easily replaced by ssreflect tactics. Also, they encourage to write
proofs that are harder to maintain.