proposition: Lemma zero_in_interval_closed_zero_open_one : (0 : [0,1)).
proof: Proof. We need to show that (0 <= 0 /\ 0 < 1). We show both (0 <= 0) and (0 < 1). - We conclude that (0 <= 0). - We conclude that (0 < 1). Qed.
imports: Coq.Reals.Reals Classical_Prop Automation Notations Tactics