Library rt.util.epsilon

Section Epsilon.

  (* ε is defined as the smallest positive number. *)
  Definition ε := 1.

End Epsilon.