proposition: Lemma range1zP (m : int) x : Rfloor x = m%:~R <-> (range1 m%:~R) x.
proof: Proof. split=> [<-|h]; first exact/mem_rg1_Rfloor. apply/eqP; rewrite RfloorE eqr_int; apply/eqP/(@range1z_inj x) => //. by rewrite /range1/mkset -RfloorE mem_rg1_Rfloor. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid