proposition: Theorem inbetween_ex : forall d u l, (d < u)%R -> exists x, inbetween d u x l.
proof: Proof. intros d u [|l] Hdu. exists d. now constructor. exists (d + match l with Lt => 1 | Eq => 2 | Gt => 3 end / 4 * (u - d))%R. constructor. set (v := (match l with Lt => 1 | Eq => 2 | Gt => 3 end / 4)%R). assert (0 < v < 1)%R. split. unfold v, Rdiv. apply Rmult_lt_0_compat. case l ; now apply IZR_lt. apply Rinv_0_lt_compat. now apply IZR_lt. unfold v, Rdiv. apply Rmult_lt_reg_r with 4%R. now apply IZR_lt. rewrite Rmult_assoc, Rinv_l. rewrite Rmult_1_r, Rmult_1_l. case l ; now apply IZR_lt. apply Rgt_not_eq. now apply IZR_lt. split. apply Rplus_lt_reg_r with (d * (v - 1))%R. ring_simplify. rewrite Rmult_comm. now apply Rmult_lt_compat_l. apply Rplus_lt_reg_l with (-u * v)%R. replace (- u * v + (d + v * (u - d)))%R with (d * (1 - v))%R by ring. replace (- u * v + u)%R with (u * (1 - v))%R by ring. apply Rmult_lt_compat_r. apply Rplus_lt_reg_r with v. now ring_simplify. exact Hdu. set (v := (match l with Lt => 1 | Eq => 2 | Gt => 3 end)%R). rewrite <- (Rcompare_plus_r (- (d + u) / 2)). rewrite <- (Rcompare_mult_r 4). 2: now apply IZR_lt. replace (((d + u) / 2 + - (d + u) / 2) * 4)%R with ((u - d) * 0)%R by field. replace ((d + v / 4 * (u - d) + - (d + u) / 2) * 4)%R with ((u - d) * (v - 2))%R by field. rewrite Rcompare_mult_l. 2: now apply Rlt_Rminus. rewrite <- (Rcompare_plus_r 2). ring_simplify (v - 2 + 2)%R (0 + 2)%R. unfold v. case l ; apply Rcompare_IZR. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Float_prop