feat: port all missing theorems in BI/DerivedLaws.lean and BI/DerivedLawsLater.lean

[alvinylt]

Description

Port all missing theorems and instances in BI/DerivedLaws.lean and BI/DerivedLawsLater.lean.

Checklist of theorems and instances being ported

• bi.and_parallel
• bi.bi_or_monoid
• bi.decide_bi_True
• bi.decide_emp
• bi.entails_anti_sym (already exists, added missing rocq_alias annotation)
• bi.entails_impl
• bi.equiv_entails_2 (ignored, the BiEntails constructor) can be used directly)
• bi.equiv_iff
• bi.exist_wand_forall
• bi.from_option_persistent
• bi.iff_equiv
• bi.iff_sym
• bi.iff_trans
• bi.impl_alt
• bi.impl_entails
• bi.impl_wand
• bi.impl_wand_2
• bi.impl_wand_intuitionistically
• bi.intuitionistically_alt_fixpoint
• bi.intuitionistically_intro
• bi.limit_preserving_emp_valid
• bi.persistent_absorbingly_affinely
• bi.persistent_and_sep_assoc
• bi.persistent_impl_wand_affinely
• bi.persistent_sep_dup
• bi.persistent_sep_dup_1
• bi.pure_flip_mono (ignored, specific to the Proper type class in Rocq)
• bi.pure_impl_forall
• bi.pure_wand_forall
• bi.wand_iff_sym
• bi.wand_iff_trans
• bi.laterN_iter (ignored, laterN in Lean is itself defined using Nat.repeat, Convert LaterN to use Nat.repeat instead of recursion #324)
• bi.löb_alt_wand
• bi.not_not_later_False

The theorem bi.wandM_sound is ported in #470.

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

[markusdemedeiros]

I did a pass just on GitHub. If you are too time-constrained right now with proofmode changes, I can also make the fixes, but otherwise I think it is good to get some practice making these basic refactoring changes to match our idioms.

[alvinylt]

Please find the fixes addressing the review comments in the latest commits.

There are also many existing proofs that could be better presented in calc style. Let me know if you'd like me to refactor those as well.

Once the remaining PRs for the IPM tactics are merged, I plan to go through the entire ProofMode directory for checks. If we can get the linter working by then, the ProofMode directory can be the first part of the codebase where we enforce the style rules strictly.

[markusdemedeiros]

Great work, thank you! Yes, I agree that there are quite a few places in the repo which should get a second look--usually I think this happens when reviewers are overwhelmed, at least that's where some of my lax reviews have came from in the past. Either way, I think that documenting style problems eagerly is a good way to make future reviews (and reviewers :p) more efficient.