proposition: Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p.
proof: Proof. unfold floor. intros p; induction p as [p [IH1p IH2p]|p [IH1p IH2]|]; simpl. - rewrite !Pos2Z.inj_xI, (Pos2Z.inj_xO (xO _)), Pos2Z.inj_xO. split. + apply Z.le_trans with (2 * Z.pos p); auto with zarith. + apply Z.lt_le_trans with (2 * (Z.pos p + 1)). * rewrite Z.mul_add_distr_l, Z.mul_1_r. apply Zplus_lt_compat_l; red; auto with zarith. * apply Z.mul_le_mono_nonneg_l; auto with zarith. rewrite Z.add_1_r; apply Zlt_le_succ; auto. - rewrite (Pos2Z.inj_xO (xO _)), (Pos2Z.inj_xO p), Pos2Z.inj_xO. split; auto with zarith. - split; auto with zarith; red; auto. Qed.
imports: ZArithRing ZArith_base Wf_nat