proposition: Lemma pos_recip_compat (x : F) (Px : 0 < x) : 0 < //(x;positive_apart_zero x Px).
proof: Proof. apply (strictly_order_reflecting (x *.)). rewrite mult_0_r. rewrite (recip_inverse' x). apply lt_0_1. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.fields HoTT.Classes.orders.rings