proposition: Lemma range1z_inj x (m1 m2 : int) : (range1 m1%:~R) x -> (range1 m2%:~R) x -> m1 = m2.
proof: Proof. move=> /andP[m1x x_m1] /andP[m2x x_m2]. wlog suffices: m1 m2 m1x {x_m1 m2x} x_m2 / (m1 <= m2). by move=> ih; apply/eqP; rewrite eq_le !ih. rewrite -(lerD2r 1) lezD1 -(@ltr_int R) intrD. exact/(le_lt_trans m1x). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid