proposition: Lemma MinT_MaxT : (MinT <= MaxT)%R.
proof: Proof. unfold MinT in |- *; pattern MaxT at 2 in |- *; rewrite <- (Rplus_0_r MaxT). unfold Rminus in |- *; apply Rplus_le_compat_l. unfold tstep in |- *; rewrite <- Ropp_0; left; apply Ropp_lt_gt_contravar; apply Rinv_0_lt_compat; prove_sup. Qed.
imports: Reals trajectory_const rrho trajectory_def