proposition: Lemma D_Rs_0_strong : (0 < derive_pt Rs 0 (Rs_derivable 0))%R.
proof: Proof. case (Rtotal_order 0 (derive_pt Rs 0 (Rs_derivable 0%R))); intro. assumption. elim H; intro. generalize (Rsqr_DRs 0); intro H1; rewrite <- H0 in H1; rewrite Rs_0 in H1; repeat rewrite Rsqr_0 in H1; rewrite Rplus_0_l in H1; rewrite Rmult_0_l in H1; generalize (eq_sym 0 (Rsqr (vi intr)) H1). clear H1; intro H1; generalize (Rsqr_eq_0 (vi intr) H1). intro H2; generalize (TypeSpeed_pos (vi intr)); intro H3; rewrite H2 in H3; elim (Rlt_irrefl 0 H3). generalize D_Rs_0; intro H1; elim (Rlt_irrefl 0 (Rle_lt_trans 0 (derive_pt Rs 0 (Rs_derivable 0%R)) 0 H1 H0)). Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho