proposition: Lemma ypt : forall t : R, (0 <= t)%R -> (rho_vi * t <= PI / 2)%R -> (hy t - hy 0 <= yp t - yp 0 <= hy 0 - hy t)%R.
proof: Proof. Proof with trivial. intros; split... apply (IAF_var yp hy 0 t yp_derivable hy_derivable H)... intros; elim H1; intros... generalize (Dyp0_PI2 c H2 (Rle_trans (rho_vi * c) (rho_vi * t) (PI / 2) (rho_t_le c t H3) H0)); intro... elim H4; intros... cut (derive_pt hy c (hy_derivable c) = (- (vi intr * sin (rho_vi * c)))%R)... intro... rewrite <- H7 in H5... rewrite Dhy; ring... replace (hy 0 - hy t)%R with ((- hy)%F t - (- hy)%F 0)%R... apply (IAF_var (- hy)%F yp 0 t (derivable_opp hy hy_derivable) yp_derivable H)... intros; elim H1; intros... generalize (Dyp0_PI2 c H2 (Rle_trans (rho_vi * c) (rho_vi * t) (PI / 2) (rho_t_le c t H3) H0)); intro... elim H4; intros... cut ((- derive_pt hy c (hy_derivable c))%R = (vi intr * sin (rho_vi * c))%R)... intro; rewrite <- H7 in H6... replace (derive_pt (- hy) c (derivable_opp hy hy_derivable c)) with (derive_pt (- hy) c (derivable_pt_opp hy c (hy_derivable c))); [ idtac | apply pr_nu ]... rewrite (derive_pt_opp hy c (hy_derivable c))... rewrite Dhy; ring... unfold opp_fct in |- *; ring... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega