proposition: Lemma pi4_mul2 : forall prec, F.valid_ub (F.mul_UP prec (upper (T.pi4 prec)) (F.fromZ 2)) = true /\ le_upper (Xreal (PI/2))%XR (F.toX (F.mul_UP prec (upper (T.pi4 prec)) (F.fromZ 2))).
proof: Proof. intros prec. unfold F.is_non_neg, F.is_non_pos, F.is_non_pos_real, F.is_non_neg_real. assert (H1 := T.pi4_correct prec). assert (H2 := proj2 (T.J.contains_le _ _ H1)). elim (F.mul_UP_correct prec (upper (T.pi4 prec)) (F.fromZ 2)). - intros H3 H4. split. exact H3. apply le_upper_trans with (2 := H4). clear -H2. destruct F.toX as [|pu]. easy. rewrite F.fromZ_correct by easy. simpl in *. lra. - unfold F.is_non_neg'. left ; split. revert H2. change T.I.F.convert with F.toX. rewrite valid_ub_upper, T.I.upper_correct by (eexists ; exact H1). destruct T.I.convert as [|l [|u]] ; try easy. apply Rle_trans, Rlt_le, PI4_RGT_0. rewrite F.fromZ_correct by easy. now apply IZR_le. Qed.
imports: Coq(Reals Psatz) Xreal Basic Sig Interval Float Transcend