proposition: Lemma u_stric_pos : forall (eps : posreal) (t : R), (0 < u eps t)%R.
proof: Proof. intros; unfold u in |- *; apply sqrt_lt_R0; apply Rplus_le_lt_0_compat; [ apply Rplus_le_le_0_compat; apply Rle_0_sqr | apply Rsqr_pos_lt; red in |- *; intro H; generalize (cond_pos eps); intro H0; rewrite H in H0; elim (Rlt_irrefl 0 H0) ]. Qed.
imports: Reals trajectory_const rrho trajectory_def constants