proposition: Lemma L : Rsqr l = (Rsqr (xe - xi intr 0) + Rsqr (ye - yi intr 0))%R.
proof: Proof. rewrite xe_0; rewrite ye_0; unfold Rminus in |- *; rewrite <- (Rplus_comm (- (l * sin beta))); repeat rewrite Rplus_assoc; repeat rewrite Rplus_opp_r; repeat rewrite Rplus_0_r; rewrite <- Rsqr_neg; repeat rewrite Rsqr_mult; rewrite <- (Rmult_comm (Rsqr (sin beta))); rewrite sin2; unfold Rminus in |- *; rewrite Rmult_plus_distr_r; ring. Qed.
imports: Bool Reals trajectory_const rrho trajectory_def constants ycngftys ycngstys Omega