proposition: Lemma recip_resp_pos : forall (y : R) y_, [0] [<] y -> [0] [<] ([1][/] y[//]y_).
proof: Proof. intros. cut ([0] [<] ([1][/] y[//]y_) or ([1][/] y[//]y_) [<] [0]). intros H0. elim H0; clear H0; intros H0. auto. exfalso. apply (less_irreflexive_unfolded R [0]). eapply less_transitive_unfolded. 2: apply H0. cut ([1] [<] ([0]:R)). intro H1. elim (less_antisymmetric_unfolded _ _ _ (pos_one _) H1). astepl ([--]([--][1]:R)). astepr ([--]([0]:R)). apply inv_resp_less. rstepr (y[*][--]([1][/] y[//]y_)). apply mult_resp_pos. auto. astepl ([--]([0]:R)). apply inv_resp_less. auto. apply ap_imp_less. apply ap_symmetric_unfolded. apply div_resp_ap_zero_rev. apply ring_non_triv. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)