proposition: Lemma recip_resp_leEq : forall (x y : R) x_ y_, [0] [<] y -> y [<=] x -> ([1][/] x[//]x_) [<=] ([1][/] y[//]y_).
proof: Proof. intros x y x_ y_ H. do 2 rewrite -> leEq_def. intros H0 H1. apply H0. cut (([1][/] x[//]x_) [#] [0]). intro x'_. cut (([1][/] y[//]y_) [#] [0]). intro y'_. rstepl ([1][/] [1][/] x[//]x_[//]x'_). rstepr ([1][/] [1][/] y[//]y_[//]y'_). apply recip_resp_less. apply recip_resp_pos; auto. auto. apply div_resp_ap_zero_rev. apply ring_non_triv. apply div_resp_ap_zero_rev. apply ring_non_triv. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)