proposition: Theorem Rlt_increasing : forall (f f' : R -> R) (a b : R), (a <= b)%R -> (forall x : R, (a <= x)%R -> (x <= b)%R -> derivable_pt_lim f x (f' x)) -> (forall x : R, (a <= x)%R -> (x <= b)%R -> (0 <= f' x)%R) -> (0 < f a)%R -> (0 < f b)%R.
proof: Proof. intros f f' a b H H0 H1 H2. case (Rtotal_order a b); intros H'2. case (MVT_cor2 f f' a b); auto. intros c (H3, H4); auto. intros c (H3, (H4, H5)). replace (f b) with (f a + (f b - f a))%R; [ rewrite H3 | ring ]. apply Rplus_lt_le_0_compat; auto with real. apply Rmult_le_pos; auto with real. case H'2; intros H'3. rewrite <- H'3; auto. Contradict H'3; auto with real. unfold Rgt in |- *; apply Rle_not_lt; auto. Qed.
imports: Coq(ZArith Classical_Prop) Coq(Rbase Rfunctions Ranalysis Rtrigo)