proposition: Lemma D_Rs_pos_non_null : forall t : R, (0 < t)%R -> (forall x : R, (0 < x < t)%R -> (0 < derive_pt Rs x (Rs_derivable x))%R) -> (0 < Rs t)%R.
proof: Proof. intros; generalize (derive_increasing_interv 0 t Rs Rs_derivable H H0); intros; cut (0 <= 0 <= t)%R; [ cut (0 <= t <= t)%R; [ intros; rewrite <- Rs_0; apply (H1 0%R t H3 H2 H) | split; [ left; assumption | right; reflexivity ] ] | split; [ right; reflexivity | left; assumption ] ]. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho