proposition: Lemma MinT_is_pos : (0 < MinT)%R.
proof: Proof. Proof with trivial. unfold MinT in |- *; unfold MaxT, tstep in |- *; apply Rmult_lt_reg_l with 2%R... prove_sup... rewrite Rmult_0_r; rewrite Rmult_minus_distr_l; rewrite <- Rinv_r_sym... apply Rlt_trans with 1%R; prove_sup... Qed.
imports: Reals trajectory_const rrho trajectory_def