feat: add ExceptConds.and_elim_left/right

[kim-em]

This PR adds general projection lemmas for ExceptConds conjunction:

• ExceptConds.and_elim_left: (x ∧ₑ y) ⊢ₑ x
• ExceptConds.and_elim_right: (x ∧ₑ y) ⊢ₑ y

The existing and_true, true_and, and_false, false_and are refactored as one-line corollaries.

Suggested by @sgraf812 in https://github.com/leanprover-community/cslib/pull/376#discussion_r2066993469.

🤖 Prepared with Claude Code

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cda84702e9b31165f1f83c657b532f36f34e0bd0 --onto 87ec768a509c45987a7d73258da0cc1ef047925c. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-02 06:34:29)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 530925c69b15c3bbe3af4ba1380e11f581be8cba --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-04 00:48:14)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase cda84702e9b31165f1f83c657b532f36f34e0bd0 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-03-02 06:34:30)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 530925c69b15c3bbe3af4ba1380e11f581be8cba --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-04 00:48:16)

[sgraf812]

Thanks!