Lemma isValidFloatDecidable : forall r,
  {isValidFloat r}+{~isValidFloat r}.
Proof.
  (** Proof omitted for brevity. *)
Qed.
