proposition: Lemma d_l_beta : Rsqr d = (Rsqr (ve * T) + Rsqr l - 2 * ve * T * l * cos beta)%R.
proof: Proof. Proof with trivial. unfold d in |- *; unfold Die in |- *; rewrite Rsqr_sqrt... replace (xi intr 0 - x (tr evad) 0)%R with (xi intr 0 - xe + (xe - x (tr evad) 0))%R... replace (yi intr 0 - y (tr evad) 0)%R with (yi intr 0 - ye + (ye - y (tr evad) 0))%R... repeat rewrite Rsqr_plus; cut ((ye - y (tr evad) 0)%R = 0%R)... intro; rewrite H; repeat rewrite Rmult_0_r; rewrite Rsqr_0; repeat rewrite Rplus_0_r; cut ((xe - x (tr evad) 0)%R = (ve * T)%R)... intro; rewrite H0; replace (Rsqr (xi intr 0 - xe) + Rsqr (ve * T) + 2 * (xi intr 0 - xe) * (ve * T) + Rsqr (yi intr 0 - ye))%R with (Rsqr (ve * T) + (Rsqr (xi intr 0 - xe) + Rsqr (yi intr 0 - ye)) + 2 * (xi intr 0 - xe) * (ve * T))%R... cut (Rsqr l = (Rsqr (xi intr 0 - xe) + Rsqr (yi intr 0 - ye))%R)... intro; rewrite <- H1; rewrite xe_0; ring... unfold l in |- *; unfold Die in |- *; rewrite Rsqr_sqrt; [ unfold xe, ye in |- * | apply Rplus_le_le_0_compat; apply Rle_0_sqr ]... ring... unfold xe, ve in |- *; rewrite (tr_cond1 evad); ring... unfold ye, ve in |- *; rewrite (tr_cond2 evad); unfold Rminus in |- *; rewrite Rplus_opp_r... ring... ring... apply Rplus_le_le_0_compat; apply Rle_0_sqr... Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega