proposition: Lemma in_segmentDgt0Pr x y z : reflect (forall e, e > 0 -> y \in `[x - e, z + e]) (y \in `[x, z]).
proof: Proof. apply/(iffP idP)=> [xyz e /[dup] e_gt0 /ltW e_ge0 | xyz_e]. by rewrite in_itv /= lerBDr !ler_wpDr// (itvP xyz). by rewrite in_itv /= ; apply/andP; split; apply/ler_addgt0Pr => ? /xyz_e; rewrite in_itv /= lerBDr => /andP []. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)