Definition isNormalized (x : R) : Prop :=
  0 <= x /\ x <= 1.
