proposition: Lemma singleton_interval r a: order r -> inc a (substrate r) -> singletonp (interval_cc r a a).
proof: Proof. move=> or asr; exists a; apply: set1_pr. by apply:Zo_i=> //;split => //; order_tac. move=> z /Zo_P [_ [p1 p2]]; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)