proposition: Lemma eps_div_leEq_eps : forall (eps d : R) d_, [0] [<=] eps -> [1] [<=] d -> (eps[/] d[//]d_) [<=] eps.
proof: Proof. intros. apply shift_div_leEq'. apply less_leEq_trans with ([1]:R). apply pos_one. assumption. astepl ([1][*]eps). apply mult_resp_leEq_rht. assumption. assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)