proposition: Lemma Rinv_le_contravar : forall x y, 0 < x -> x <= y -> / y <= / x.
proof: Proof. intros x y H1 [H2|H2]. apply Rlt_le. apply Rinv_lt_contravar with (2 := H2). apply Rmult_lt_0_compat with (1 := H1). now apply Rlt_trans with x. rewrite H2. apply Rle_refl. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)