Improve commutativity lemma for Bplus

[ak-2485]

The lemma Bplus_commut in FPCore.v was redundant. The file already imports IEEE754_extra.Bplus_commut, which proves commutativity of float add under the assumption that the payload constructor is itself commutative. More importantly, for most practical cases we only need commutativity under the assumption that the inputs are finite, where the NaN-payload function is never invoked. This PR replaces the redundant lemma with a finite-input commutativity lemma, which is both strictly weaker in assumptions and strictly more useful in downstream proofs.