(x y : F) (Px : 0 < x) (Py : 0 < y) (ltyx : y < //(x;positive_apart_zero x Px)) : x < //(y;positive_apart_zero y Py). Proof. set (apx0 := positive_apart_zero x Px). set (apy0 := positive_apart_zero y Py). change x with ((x;apx0) : ApartZero F).1. rewrite <- (recip_involutive (x;apx0)). unfold recip_on_apart; cbn. assert (ltry := pos_recip_compat y Py). rewrite (recip_irrelevant y (positive_apart_zero y Py) apy0) in ltry. change y with ((y;apy0) : ApartZero F).1 in ltyx. rewrite <- (recip_involutive (y;apy0)) in ltyx. unfold recip_on_apart in ltyx; cbn in ltyx. rewrite (recip_irrelevant (//(y;apy0)) (recip_apart y apy0) (positive_apart_zero (// (y; apy0)) ltry)) in ltyx. assert (ltxy := flip_lt_recip_l (// (x; apx0)) (// (y; apy0)) ltry ltyx). cbn in ltxy. rewrite (recip_irrelevant (//(x;apx0)) (positive_apart_zero (// (x; apx0)) (transitivity (pos_recip_compat (// (y; apy0)) ltry) ltyx)) (recip_apart x apx0)) in ltxy. assumption. Qed.
Require Import