proposition: Lemma flip_le_dec_recip x y : 0 < y -> y ≤ x -> /x ≤ /y.
proof: Proof. intros E1 E2. apply (order_reflecting_pos (.*.) x). - apply lt_le_trans with y;trivial. - rewrite dec_recip_inverse. + apply (order_reflecting_pos (.*.) y);trivial. 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. apply lt_le_trans with y;trivial. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.orders HoTT.Classes.theory.dec_fields HoTT.Classes.orders.rings