How can I implement a notation of the form: ∀ x ≤ y ≤ .. ≤ z ≤ t, φ in Coq?
A similar notation (but without quantifiers) appears here
Notation "x ≤ y ≤ .. ≤ z ≤ t" :=
((fun b A a => a <= b /\ A b) y
.. ((fun b A a => a <= b /\ A b) z (fun b => b <= t))
.. x)
(at level 70, y at next level, z at next level, t at next level).
But I was unsuccessful in putting forall quantifiers to it.
