proposition: Theorem YCNGSTYS : forall t : R, (0 <= t)%R -> (rho (vi intr) * t < 2)%R -> (2 * r (vi intr) * sin (rho (vi intr) * (t / 2)) <= sqrt (Rsqr (xi intr t - xi intr 0) + Rsqr (yi intr t - yi intr 0)))%R.
proof: Proof. intros; generalize (rho_pos (vi intr)); intro H1; generalize (Rinv_0_lt_compat (rho (vi intr)) H1); intro H2; generalize (Rmult_lt_compat_l (/ rho (vi intr)) (rho (vi intr) * t) 2 H2 H0); intro H3; rewrite <- Rmult_assoc in H3; rewrite <- Rinv_l_sym in H3. rewrite Rmult_1_l in H3; rewrite Rmult_comm in H3; generalize (G_pos t H H3); unfold G in |- *; intro H4; generalize (Rplus_le_compat_l (F t) 0 (Rs t - F t) H4); rewrite Rplus_0_r; intro H5; unfold Rminus in H5; rewrite <- Rplus_assoc in H5; rewrite Rplus_comm in H5; rewrite <- Rplus_assoc in H5; rewrite Rplus_opp_l in H5; rewrite Rplus_0_l in H5; unfold Rs, F in H5; unfold r in |- *; assumption. red in |- *; intro H4; rewrite H4 in H1; elim (Rlt_irrefl 0 H1). Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho