proposition: Lemma range1z_inj x m1 m2 : range1 m1 x -> range1 m2 x -> m1 = m2.
proof: Proof. move=> [m1x x_m1] [m2x x_m2]. wlog suffices: m1 m2 m1x {x_m1 m2x} x_m2 / (m1 <= m2)%R. by move=> IH; apply/eqP; rewrite eq_le !IH. rewrite -(ler_add2r 1); apply/intR_ltP. by rewrite intRD1; apply: leR_lt_trans x_m2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)