Data.SBV.Examples.Misc.Floating
FP addition is not associative
assocPlus
assocPlusRegular
FP addition by non-zero can result in no change
nonZeroAddition
FP multiplicative inverses may not exist
multInverse
Effect of rounding modes
roundingAdd