proposition: Lemma floor_neq0 x : (floor x != 0) = (x < 0) || (x >= 1).
proof: Proof. apply/idP/orP => [|[x0|/le_floor r1]]; first rewrite neq_lt => /orP[x0|x0]. - by left; apply: contra_lt x0; rewrite floor_ge0. - by right; rewrite (le_trans _ (floor_le _))// ler1z -gtz0_ge1. - by rewrite lt_eqF//; apply: contra_lt x0; rewrite floor_ge0. - by rewrite gt_eqF// (lt_le_trans _ r1)// floor1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid