proposition: Lemma itvxx x : `[x, x] =i pred1 x.
proof: Proof. by move=> y; rewrite in_itv/= -eq_le eq_sym. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(div fintype bigop order ssralg finset fingroup) mathcomp(ssrnum)