proposition: Lemma cond1_0 : (- toDeg MaxBank <= 0)%R.
proof: Proof. left; rewrite <- Ropp_0; apply Ropp_lt_gt_contravar; unfold toDeg in |- *; repeat simple apply Rmult_lt_0_compat. unfold MaxBank in |- *; unfold Rdiv in |- *; apply Rmult_lt_0_compat. prove_sup. apply Rinv_0_lt_compat; prove_sup. unfold plat in |- *; prove_sup. apply Rinv_0_lt_compat; apply PI_RGT_0. Qed.
imports: Reals trajectory_const constants ails_def tau Omega