Greatly improve formal verification testing

[ChristopherRabotin]

Now that the HTML Kani report is available in the CI pipeline, it's quite easy to see what is covered and what isn't. The purpose of this issue is to increase the parts of the code that are formally verified.

• Duration formal verification
  • Verify reciprocity of constructors with their associated functions (like from_truncated_nanoseconds should match the result of try_truncated_nanoseconds)
  • to_seconds shall be tested with very high durations (and will likely exhibit the rounding errors of f64s)
  • decompose shall be tested with very high durations (there are expectations in the code but these aren't checked)
  • min and max on durations should be tested to be correct (this will require the need for the kani assumptions)
• Epoch formal verification (this is new)
  • Build an Duration::any() function for kani (take inspiration on nalgebra if needed)
  • For all time scales that support an initialization, ensure that Epoch::from_$ts$_duration(Duration::any()) returns the same Duration::any(). Skip the ET time scale because it uses a newton Raphson scheme for building durations and that may introduce an error of up to 20 nanoseconds (IIRC).
  • From all time scales that support initialization from seconds or days, repeat the test above.

[ChristopherRabotin]

The to_seconds test takes over two hours on my machine, and even then I killed it. So we'll figure this out later.