proposition: Lemma seq_step_unif_part_ex (a b : R) (eps : posreal) : {n : nat | seq_step (unif_part a b n) < eps}.
proof: Proof. destruct (nfloor_ex (Rabs ((b - a) / eps))) as [n Hn]. by apply Rabs_pos. exists n. rewrite seq_step_unif_part. rewrite Rabs_div. rewrite (Rabs_pos_eq (INR n + 1)). apply Rlt_div_l. by apply INRp1_pos. rewrite Rmult_comm -Rlt_div_l. rewrite -(Rabs_pos_eq eps). rewrite -Rabs_div. by apply Hn. by apply Rgt_not_eq, eps. by apply Rlt_le, eps. by apply eps. by apply Rlt_le, INRp1_pos. by apply Rgt_not_eq, INRp1_pos. Qed.
imports: Coq(Reals Psatz ssreflect ssrbool) mathcomp(seq) Rcomplements Rbar Lub Hierarchy