WIP: Remove `contractive_ne` and `contractive_proper` as instances.

This is a follow up of !454 (merged). It closes #321.

It removes contractive_ne and contractive_proper as instances, to be consistent with ne_proper. For all functions that are contractive, we already defined the corresponding NonExpansive and Proper instances, so these instances just caused type class search to try useless paths.

These instances are sometimes useful when considering a lemma or section with a Contractive f parameter. Hence I added contractive_ne and contractive_proper as Hint Immediate so they are only used at the leaves of type class search. I have done a similar thing for proper_ne and proper_ne_2.