proposition: Lemma D_G_pos : forall t : R, (0 <= t)%R -> (t < 2 / rho (vi intr))%R -> (G t <= 0)%R -> (0 <= derive_pt G t (G_derivable t))%R.
proof: Proof. intros. case (Rcase_abs (derive_pt G t (G_derivable t))); intro. generalize (D_G_alphas t); intro. generalize (D_Rs_pos t H H0); intro. cut (0 <= derive_pt F t (F_derivable t))%R. intro. generalize (Rs_pos t); intro. cut (0 <= F t)%R. intro. cut (derive_pt G t (G_derivable t) * (derive_pt Rs t (Rs_derivable t) + derive_pt F t (F_derivable t)) < 0)%R. intro. cut (0 <= - Rsqr (derive_pt alphas t (cond_D1 alphas t)) * G t * (Rs t + F t) + Rsqr (F t) * (Rsqr (rho (vi intr) / 2) - Rsqr (derive_pt alphas t (cond_D1 alphas t))))%R. intro. rewrite <- H2 in H8. elim (Rlt_irrefl 0 (Rle_lt_trans 0 (derive_pt G t (G_derivable t) * (derive_pt Rs t (Rs_derivable t) + derive_pt F t (F_derivable t))) 0 H8 H7)). apply Rplus_le_le_0_compat. replace (- Rsqr (derive_pt alphas t (cond_D1 alphas t)) * G t * (Rs t + F t))%R with (Rsqr (derive_pt alphas t (cond_D1 alphas t)) * - G t * (Rs t + F t))%R. repeat simple apply Rmult_le_pos. apply Rle_0_sqr. rewrite <- Ropp_0. apply Ropp_ge_le_contravar. apply Rle_ge; assumption. apply Rplus_le_le_0_compat; assumption. ring. apply Rmult_le_pos. apply Rle_0_sqr. apply Rplus_le_reg_l with (Rsqr (derive_pt alphas t (cond_D1 alphas t))). rewrite Rplus_0_r. rewrite Rplus_comm. unfold Rminus in |- *. repeat rewrite Rplus_assoc. rewrite Rplus_opp_l. rewrite Rplus_0_r. generalize (D_abs_alpha t H H0); intro. elim H8; intros. case (Rtotal_order 0 (derive_pt alphas t (cond_D1 alphas t))); intro. apply Rsqr_incr_1. assumption. left; assumption. unfold Rdiv in |- *; left; apply Rmult_lt_0_compat. apply rho_pos. apply Rinv_0_lt_compat; prove_sup0. elim H11; intros. rewrite <- H12. rewrite Rsqr_0. apply Rle_0_sqr. rewrite (Rsqr_neg (derive_pt alphas t (cond_D1 alphas t))). apply Rsqr_incr_1. rewrite <- (Ropp_involutive (rho (vi intr) / 2)). apply Ropp_ge_le_contravar. apply Rle_ge. replace (- (rho (vi intr) / 2))%R with (- rho (vi intr) / 2)%R. assumption. unfold Rdiv in |- *; ring. rewrite <- Ropp_0. apply Ropp_ge_le_contravar; apply Rle_ge; left; assumption. unfold Rdiv in |- *; left; apply Rmult_lt_0_compat. apply rho_pos. apply Rinv_0_lt_compat; prove_sup0. rewrite <- (Ropp_involutive 0). replace (derive_pt G t (G_derivable t) * (derive_pt Rs t (Rs_derivable t) + derive_pt F t (F_derivable t)))%R with (- (- derive_pt G t (G_derivable t) * (derive_pt Rs t (Rs_derivable t) + derive_pt F t (F_derivable t))))%R. apply Ropp_lt_gt_contravar. rewrite Ropp_0. apply Rmult_lt_0_compat. rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption. apply Rplus_lt_le_0_compat; assumption. ring. unfold F in |- *. repeat simple apply Rmult_le_pos. left; prove_sup0. unfold Rdiv in |- *; left; apply Rmult_lt_0_compat. apply TypeSpeed_pos. apply Rinv_0_lt_compat; apply rho_pos. apply sin_ge_0. unfold Rdiv in |- *; repeat simple apply Rmult_le_pos. left; apply rho_pos. assumption. left; apply Rinv_0_lt_compat; prove_sup0. left; apply Rlt_trans with 1%R. unfold Rdiv in |- *. apply Rmult_lt_reg_l with (2 * / rho (vi intr))%R. apply Rmult_lt_0_compat; [ prove_sup0 | apply Rinv_0_lt_compat; apply rho_pos ]. rewrite Rmult_1_r. replace (2 * / rho (vi intr) * (rho (vi intr) * (t * / 2)))%R with t. assumption. repeat rewrite Rmult_assoc. rewrite Rmult_comm. repeat rewrite Rmult_assoc. rewrite <- Rinv_l_sym. repeat rewrite <- Rmult_assoc. rewrite <- Rinv_l_sym. rewrite Rmult_1_r; symmetry in |- *; apply Rmult_1_l. red in |- *; generalize (rho_pos (vi intr)); intros; rewrite H7 in H6; elim (Rlt_irrefl 0 H6). discrR. apply Rlt_trans with (PI / 2)%R. apply Rlt_1_PI2. apply PI2_Rlt_PI. rewrite D_F. apply Rmult_le_pos. left; apply TypeSpeed_pos. apply cos_ge_0. left; apply Rlt_le_trans with 0%R. rewrite <- Ropp_0. apply Ropp_lt_gt_contravar. apply PI2_RGT_0. unfold Rdiv in |- *; repeat simple apply Rmult_le_pos. left; apply rho_pos. assumption. left; apply Rinv_0_lt_compat; prove_sup0. left; apply Rlt_le_trans with 1%R. apply Rmult_lt_reg_l with (2 / rho (vi intr))%R. unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ prove_sup0 | apply Rinv_0_lt_compat; apply rho_pos ]. rewrite Rmult_1_r. replace (2 / rho (vi intr) * (rho (vi intr) * (t / 2)))%R with t. assumption. unfold Rdiv in |- *. repeat rewrite Rmult_assoc. rewrite (Rmult_comm 2). repeat rewrite <- Rmult_assoc. rewrite <- Rinv_l_sym. repeat rewrite Rmult_assoc. rewrite <- Rinv_l_sym. rewrite Rmult_1_r; rewrite Rmult_1_l. reflexivity. discrR. red in |- *; generalize (rho_pos (vi intr)); intros; rewrite H5 in H4; elim (Rlt_irrefl 0 H4). left; apply Rlt_1_PI2. apply Rge_le. assumption. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho