proposition: Lemma init_tr_cond_theta : forall (h : TypeSpeed) (t : R), derive_pt (fun t : R => 0%R) t (init_tr_derivable_y h t) = (fun t : R => (g * (tan 0 / h))%R) t.
proof: Proof. intros; reg. unfold Rdiv in |- *; rewrite tan_0; ring. Qed.
imports: Reals trajectory_const rrho