proposition: Lemma eps_div_less_eps : forall (eps d : R) d_, [0] [<] eps -> [1] [<] d -> (eps[/] d[//]d_) [<] eps.
proof: Proof. intros. apply shift_div_less'. apply leEq_less_trans with ([1]:R). apply less_leEq; apply pos_one. assumption. astepl ([1][*]eps). apply mult_resp_less. assumption. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)