proposition: Lemma D_Rs_0 : (0 <= derive_pt Rs 0 (Rs_derivable 0))%R.
proof: Proof. case (Rtotal_order 0 (derive_pt Rs 0 (Rs_derivable 0%R))); intro. left; assumption. elim H; intro. right; assumption. generalize (derivable_derive Rs 0 (Rs_derivable 0%R)); intro; elim H1; intros l H2; rewrite H2 in H0. generalize (derive_pt_eq_1 Rs 0 l (Rs_derivable 0%R) H2); intros; cut (0 < - (l / 2))%R. intro H4; elim (H3 (- (l / 2))%R H4). intros; cut ((x / 2)%R <> 0%R). intro H6; cut (Rabs (x / 2) < x)%R. intro H7; generalize (H5 (x / 2)%R H6 H7); intro H8; rewrite Rs_0 in H8; rewrite Rplus_0_l in H8; unfold Rminus in H8; rewrite Ropp_0 in H8; rewrite Rplus_0_r in H8; generalize (Rabs_def2 (Rs (x / 2) / (x / 2) + - l) (- (l / 2)) H8); intro H9; elim H9; intros; generalize (Rplus_lt_compat_r l (Rs (x / 2) / (x / 2) + - l) (- (l / 2)) H10); rewrite Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_r; replace (- (l / 2) + l)%R with (l / 2)%R. intro H12; cut (l / 2 < 0)%R. intro H13; generalize (Rlt_trans (Rs (x / 2) / (x / 2)) (l / 2) 0 H12 H13); intro H14; unfold Rdiv in H14; cut (0 < x * / 2)%R. intro H15; generalize (Rmult_lt_compat_r (x * / 2) (Rs (x * / 2) * / (x * / 2)) 0 H15 H14); rewrite Rmult_0_l; rewrite Rmult_assoc; rewrite <- Rinv_l_sym. rewrite Rmult_1_r; intro H16; elim (Rlt_irrefl 0 (Rle_lt_trans 0 (Rs (x * / 2)) 0 (Rs_pos (x * / 2)) H16)). apply prod_neq_R0. generalize (cond_pos x); intro H16; red in |- *; intro H17; rewrite H17 in H16; elim (Rlt_irrefl 0 H16). apply Rinv_neq_0_compat; discrR. apply Rmult_lt_0_compat; [ apply (cond_pos x) | apply Rinv_0_lt_compat; prove_sup0 ]. assert (Hyp : (0 < 2)%R). prove_sup0. unfold Rdiv in |- *; generalize (Rmult_lt_compat_r (/ 2) l 0 (Rinv_0_lt_compat 2 Hyp) H0); rewrite Rmult_0_l; intro H13; exact H13. pattern l at 3 in |- *; rewrite double_var. ring. cut (0 < x / 2)%R. intro H7; apply Rabs_def1. pattern x at 1 in |- *; replace (pos x) with (2 * (x / 2))%R. pattern (x / 2)%R at 1 in |- *; replace (x / 2)%R with (x / 2 + 0)%R. replace (2 * (x / 2))%R with (x / 2 + x / 2)%R. apply Rplus_lt_compat_l; assumption. ring. apply Rplus_0_r. pattern (pos x) at 2 in |- *; rewrite double_var. ring. apply Rlt_trans with 0%R. rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; apply (cond_pos x). assumption. unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ apply (cond_pos x) | apply Rinv_0_lt_compat; prove_sup0 ]. unfold Rdiv in |- *; apply prod_neq_R0. generalize (cond_pos x); intro H6; red in |- *; intro H7; rewrite H7 in H6; elim (Rlt_irrefl 0 H6). apply Rinv_neq_0_compat; discrR. assert (Hyp : (0 < 2)%R). prove_sup0. unfold Rdiv in |- *; rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; generalize (Rmult_lt_compat_r (/ 2) l 0 (Rinv_0_lt_compat 2 Hyp) H0); rewrite Rmult_0_l; intro H4; assumption. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho