proposition: Lemma open_lemma : forall a b c, a < b -> c > 0 -> open_interval a b (a + Rmin ((b - a) /2) c).
proof: Proof. intros. assert ((b0 - a0) > 0) by lra. assert ((b0-a0) /2 > 0). apply (Rmult_gt_0_compat (/2)) in H1. now lra. now lra. split. assert (Rmin ((b0-a0) /2) c > 0). now apply Rmin_glb_lt; assumption. now lra. apply Rle_lt_trans with (a0 + (b0-a0) /2). apply Rplus_le_compat_l. now apply Rmin_l. assert (b0 - a0 - (b0-a0) /2 > 0). field_simplify. now lra. lra. Qed.
imports: Reals Lra Rfunction_classes_def Cauchy_lipschitz Rextensionality