proposition: Lemma dtheta_rho : forall (tr : Trajectory) (t : R), (- rho (h tr) <= derive_pt (theta tr) t (cond_diff (theta tr) t) <= rho (h tr))%R.
proof: Proof. intros; generalize (cond_theta tr0); intro; rewrite (H t); unfold rho in |- *; generalize (cond_phi tr0); intro; elim (H0 t); intros H1 H2; generalize MaxBank_encadr; intro H3; elim H3; intros H4 H5; split. unfold Rdiv in |- *; replace (- (g * (tan MaxBank * / h tr0)))%R with (g * (- tan MaxBank * / h tr0))%R. apply Rmult_le_compat_l. left; apply g_pos. setoid_rewrite Rmult_comm at 1 2. apply Rmult_le_compat_l. left; apply (Rinv_0_lt_compat (h tr0) (TypeSpeed_pos (h tr0))). rewrite <- tan_neg. generalize (Rlt_le (- (PI / 4)) (- MaxBank) (Ropp_lt_gt_contravar MaxBank (PI / 4) H5)); intro H6; generalize (Ropp_lt_gt_contravar 0 MaxBank H4); rewrite Ropp_0; intro H7; generalize (Rlt_le (- MaxBank) (PI / 4) (Rlt_trans (- MaxBank) 0 (PI / 4) H7 PI4_RGT_0)); intro H8; generalize (Rlt_le (phi tr0 t) (PI / 4) (Rle_lt_trans (phi tr0 t) MaxBank (PI / 4) H2 H5)); intro H9; generalize (Rle_trans (- (PI / 4)) (- MaxBank) (phi tr0 t) H6 H1); intro H10; apply tan_incr_1; assumption. replace (- tan MaxBank)%R with (-1 * tan MaxBank)%R. repeat rewrite <- Rmult_assoc; rewrite <- (Rmult_comm (-1)); repeat rewrite <- Rmult_assoc; replace (- (g * tan MaxBank * / h tr0))%R with (-1 * g * tan MaxBank * / h tr0)%R; [ reflexivity | ring ]. ring. apply Rmult_le_compat_l; [ left; apply g_pos | unfold Rdiv in |- *; rewrite (Rmult_comm (tan MaxBank)); rewrite (Rmult_comm (tan (phi tr0 t))); apply Rmult_le_compat_l; [ left; apply (Rinv_0_lt_compat (h tr0) (TypeSpeed_pos (h tr0))) | generalize (Rlt_le MaxBank (PI / 4) H5); intro H6; generalize (Rle_trans (phi tr0 t) MaxBank (PI / 4) H2 H6); intro H7; generalize PI4_RGT_0; intro H8; generalize (Ropp_lt_gt_contravar 0 (PI / 4) H8); rewrite Ropp_0; intro H9; generalize (Rlt_le (- (PI / 4)) MaxBank (Rlt_trans (- (PI / 4)) 0 MaxBank H9 H4)); intro H10; generalize (Ropp_le_ge_contravar MaxBank (PI / 4) H6); intro H11; generalize (Rge_le (- MaxBank) (- (PI / 4)) H11); intro H12; generalize (Rle_trans (- (PI / 4)) (- MaxBank) (phi tr0 t) H12 H1); intro H13; apply tan_incr_1; assumption ] ]. Qed.
imports: Reals trajectory_const rrho