proposition: Lemma flip_lt_dec_recip x y : 0 < y -> y < x -> /x < /y.
proof: Proof. intros E1 E2. assert (0 < x) by (transitivity y;trivial). apply (strictly_order_reflecting (x *.)). rewrite dec_recip_inverse. - apply (strictly_order_reflecting (y *.)). rewrite (commutativity x), simple_associativity, dec_recip_inverse. + rewrite mult_1_l,mult_1_r. trivial. + apply lt_ne_flip. trivial. - apply lt_ne_flip;trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.dec_fields HoTT.Classes.orders.rings