proposition: Lemma increasing_decreasing_opp : forall f:R -> R, increasing f -> decreasing (- f)%F.
proof: Proof. unfold increasing, decreasing, opp_fct; intros; generalize (H x y H0); intro; apply Ropp_ge_le_contravar; apply Rle_ge; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra