proposition: Lemma mem_zspan xmin xmax x : (x \in zspan xmin xmax) = (xmin <= x < xmax).
proof: Proof. rewrite -[xmax in RHS](subrK xmin) -ltr_subl_addr -subr_ge0 /zspan /zwidth. case: {xmax}(xmax - xmin) => n; last by case: (x - xmin). elim: n xmin => [|n IHn] x0; first by rewrite ltNge andbN. rewrite inE -subr_eq0 {}IHn opprD addrA ler_subr_addl ltr_subl_addl. by rewrite orb_andr eq_sym -le_eqVlt; case: eqP => // <-. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div choice order ssralg ssrnum ssrint intdiv) fourcolor(hypermap)