proposition: Lemma Rlt_1_PI2 : (1 < PI / 2)%R.
proof: Proof. generalize PI_approx; intro; elim H; intros. apply Rlt_le_trans with (PI_lb / 2)%R. unfold PI_lb in |- *; unfold Rdiv in |- *; apply Rmult_lt_reg_l with 2%R. prove_sup. rewrite Rmult_1_r; rewrite <- Rmult_assoc; rewrite Rinv_r_simpl_m; [ prove_sup | discrR ]. left; unfold Rdiv in |- *; repeat rewrite <- (Rmult_comm (/ 2)); apply Rmult_lt_compat_l; [ apply Rinv_0_lt_compat; prove_sup | assumption ]. Qed.
imports: Reals trajectory_def trajectory_const constants ycngftys rrho