chore: bool and prop lemmas for Mathlib compatibility and improved confluence

[joehendrix]

This adds a number of lemmas for simplification of Bool and Prop terms. It pulls lemmas from Mathlib and adds additional lemmas where confluence or consistency suggested they are needed.

It has been tested against Mathlib using some automated test infrastructure.

That testing module is not yet included in this PR, but will be included as part of this.

Note. There are currently some comments saying the origin of the simp rule. These will be removed prior to merging, but are added to clarify where the rule came from during review.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e73495e5a6059bfebeed65032fed2b9a1b6933c9 --onto 88fbe2e5313bb418abdb035c48cae2680ea9bcea. (2024-02-26 19:59:43)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 755de48ff318dcf370037c969374148dc56d458e --onto a23292f0491c7373bd6ec4ca44d030ded15d1719. (2024-02-29 05:31:13)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7e944c1a309728581257cb6351c9bc0b9c741b7e --onto 43d6eb144e7a84af7c6eb40e60c9d2538367d6eb. (2024-03-01 17:12:53)
• ❗ Std/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e814fc859e8feb2c7e1c94a1d8b05e8b27149e62 --onto e6d6855a854cbde5bf7d99c7997443427dcfdba9. (2024-03-04 22:22:45)