Add `Proper`s for maps, and generalise existing ones. Add tests to check that the old ones can be derived.

Rename `option_mbind_proper` → `option_bind_proper` and `option_mjoin_proper` → `option_join_proper`.

Rename `map_disjoint_filter` → `map_disjoint_filter_complement` and `map_union_filter` → `map_filter_union_complement`.

Rename `Permutation_nil` and `Permutation_singleton` into `Permutation_nil_r` and `Permutation_singleton_r`.

Add lemmas `Permutation_nil_l` and `Permutation_singleton_l`.

Naming scheme: `operation_Permutation_{Proper,inj,inj_l,inj_r}`.