proposition: Lemma recip_resp_less : forall (x y : R) x_ y_, [0] [<] x -> x [<] y -> ([1][/] y[//]y_) [<] ([1][/] x[//]x_).
proof: Proof. intros. cut ([0] [<] x[*]y). intro. cut (x[*]y [#] [0]). intro H2. rstepl (x[*]([1][/] x[*]y[//]H2)). rstepr (y[*]([1][/] x[*]y[//]H2)). apply mult_resp_less. auto. apply recip_resp_pos. auto. apply Greater_imp_ap. auto. apply mult_resp_pos. auto. apply less_leEq_trans with x; try apply less_leEq; auto. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)