x y (Py : 0 < y) (ltyx : //(y;positive_apart_zero y Py) < x) : let apx0 := positive_apart_zero x (transitivity (pos_recip_compat y Py) ltyx) in //(x;apx0) < y. Proof. set (apy0 := positive_apart_zero y Py). set (eq := recip_involutive (y;apy0)). set (eq' := ap pr1 eq). cbn in eq'. rewrite <- eq'. unfold recip_on_apart. set (ltyx2 := ltyx). unfold ltyx2. rewrite (recip_irrelevant y (positive_apart_zero y Py) apy0) in ltyx2. set (ltyx_recips := flip_lt_recip x (// (y; apy0)) (pos_recip_compat y Py) ltyx2). cbn in ltyx_recips. rewrite (recip_irrelevant x _ (positive_apart_zero x (transitivity (pos_recip_compat y Py) ltyx))) in ltyx_recips. cbn. rewrite (recip_irrelevant (//(y;apy0)) _ (recip_apart y apy0)) in ltyx_recips. assumption. Qed.
Require Import