Lemma inRangeDecidable : forall (x low high : Z), {low <= x /\ x <= high}+{~(low <= x /\ x <= high)}.
