proposition: Theorem mul2_correct : forall prec xi x, contains (convert xi) x -> contains (convert (mul2 prec xi)) (Xmul x (Xreal 2)).
proof: Proof. intros prec [ | xl xu]. easy. intros [|x]; unfold convert; [now case (_ && _)|]. case_eq (F.valid_lb xl); [|intros _ [H0 H1]; exfalso; lra]. case_eq (F.valid_ub xu); [|intros _ _ [H0 H1]; exfalso; lra]. intros Vxu Vxl [Hxl Hxu]. simpl. unfold c2. elim (F.mul_DN_correct prec xl (F.fromZ 2)); [intros Vl Hl; rewrite Vl|]. { elim (F.mul_UP_correct prec xu (F.fromZ 2)); [intros Vu Hu; rewrite Vu|]. { split. { xreal_tac2. revert Hl; rewrite F.fromZ_correct by easy. unfold le_lower, le_upper; simpl. now xreal_tac2; simpl; [|lra]. } xreal_tac2. revert Hu; rewrite F.fromZ_correct by easy. unfold le_upper. now xreal_tac2; simpl; [|lra]. } unfold F.is_non_neg', F.is_non_pos', F.is_non_neg_real, F.is_non_pos_real. rewrite Vxu. rewrite F.fromZ_correct by easy. xreal_tac2; [now left; repeat split; lra|]. case (Rlt_or_le 0 r); intro Hr. { left; repeat split; lra. } do 2 right; left; lra. } unfold F.is_non_neg', F.is_non_pos', F.is_non_neg_real, F.is_non_pos_real. rewrite Vxl. rewrite F.fromZ_correct by easy. xreal_tac2; [now do 3 right; repeat split; lra|]. case (Rlt_or_le 0 r); intro Hr. { left; repeat split; lra. } do 3 right; repeat split; lra. Qed.
imports: Coq(Bool Reals Psatz) Flocq(Raux) Stdlib Xreal Basic Sig Interval