proposition: Lemma D_alphas_0 : (2 * derive_pt alphas 0 (cond_D1 alphas 0))%R = derive_pt thetat 0 (thetat_derivable 0%R).
proof: Proof. generalize (D_Rs_2 0); intro; rewrite Rs_0 in H; rewrite Ropp_0 in H; rewrite Rmult_0_l in H; generalize (Rmult_integral (derive_pt Rs 0 (Rs_derivable 0%R)) (2 * derive_pt alphas 0 (cond_D1 alphas 0%R) - derive_pt thetat 0 (thetat_derivable 0%R)) H); intro H1; elim H1; intro; generalize D_Rs_0_strong; intro. rewrite H0 in H2; elim (Rlt_irrefl 0 H2). generalize (Rminus_diag_uniq_sym (derive_pt thetat 0 (thetat_derivable 0%R)) (2 * derive_pt alphas 0 (cond_D1 alphas 0%R)) H0); intro; symmetry in |- *; assumption. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho