proposition: Lemma increasing_decreasing : forall f:R -> R, increasing f -> decreasing f -> constant f.
proof: Proof. unfold increasing, decreasing, constant; intros; case (Rtotal_order x y); intro. - generalize (Rlt_le x y H1); intro; apply (Rle_antisym (f x) (f y) (H x y H2) (H0 x y H2)). - elim H1; intro. + rewrite H2; reflexivity. + generalize (Rlt_le y x H2); intro; symmetry ; apply (Rle_antisym (f y) (f x) (H y x H3) (H0 y x H3)). Qed.
imports: Rbase Rfunctions Ranalysis1 Rtopology Lra