proposition: Lemma Rs_0 : Rs 0 = 0%R.
proof: Proof. unfold Rs in |- *; unfold Rminus in |- *; repeat rewrite Rplus_opp_r; repeat rewrite Rsqr_0; rewrite Rplus_0_r; rewrite sqrt_0; reflexivity. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho