[Farith2] Runtime checks with assertions

• Add Assert.v module to describe runtime assertions
• Rename some theorem in Correction_thm.v for better readability
• Minimal implementation of a GenericFloat module using runtime assertions