proposition: Lemma d_u : forall eps : posreal, derivable (fun t : R => u eps t).
proof: Proof. intro. unfold u in |- *; unfold derivable in |- *; intro. reg. apply yP_derivable. apply xP_derivable. apply Rle_lt_trans with (Rsqr (xP x) + Rsqr (yP x))%R. apply Rplus_le_le_0_compat; apply Rle_0_sqr. rewrite Rplus_assoc. apply Rplus_lt_compat_l. pattern (Rsqr (yP x)) at 1 in |- *; rewrite <- Rplus_0_r. apply Rplus_lt_compat_l. apply Rsqr_pos_lt. red in |- *; intro; assert (H0 := cond_pos eps); rewrite H in H0; elim (Rlt_irrefl _ H0). Qed.
imports: Reals trajectory_const rrho trajectory_def constants