proposition: Lemma strictincreasing_strictdecreasing_opp : forall f:R -> R, strict_increasing f -> strict_decreasing (- f)%F.
proof: Proof. unfold strict_increasing, strict_decreasing, opp_fct; intros; generalize (H x y H0); intro; apply Ropp_lt_gt_contravar; assumption. Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra