proposition: Lemma init_tr_cond_phi : forall t : R, (- MaxBank <= (fun t : R => 0) t)%R /\ ((fun t : R => 0) t <= MaxBank)%R.
proof: Proof. intros; simpl in |- *; cut (0 < MaxBank)%R. split. left; rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; assumption. left; assumption. unfold MaxBank in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat; [ prove_sup | apply Rinv_0_lt_compat; prove_sup ]. Qed.
imports: Reals trajectory_const rrho