Add two categories of finitely generated projective modules

[ScriptRaccoon]

This PR adds two instances of the category of finitely generated projective modules over a ring: one over the ring of integers and one over the ring of dual numbers. All properties have been decided.

We now have exactly 100 categories in the database. 🎉

One could try to add the category Proj_fg(R) of finitely generated projective modules over a ring more generally, but many properties cannot be decided in this generality. The two examples already indicate a significant difference. For example, Proj_fg(R[ε]) is balanced, but Proj_fg(Z) is not.

New property combinations

• The category Proj_fg(Z) = FreeAb_fg provides an example of an additive category that is not balanced and does not have coproducts.
• The category Proj_fg(R[ε]) provides an example of an additive, normal, and conormal category that is not abelian.

For combinations of the form "p and not q", the number of consistent yet unwitnessed combinations went down from 733 to 725. The combinations script shows:

Found 4 unique witnessed combinations for category with ID "FreeAb_fg":
- essentially countable ∧ ¬effective cocongruences
- essentially countable ∧ ¬effective congruences
- self-dual ∧ ¬effective cocongruences
- self-dual ∧ ¬effective congruences

Found 4 unique witnessed combinations for category with ID "Proj_fg(Re)":
- normal ∧ ¬coreflexive equalizers
- normal ∧ ¬reflexive coequalizers
- conormal ∧ ¬coreflexive equalizers
- conormal ∧ ¬reflexive coequalizers