proposition: Lemma one_in_complement_interval_closed_zero_open_one : (1 : ℝ \ [0,1)).
proof: Proof. We need to show that (~ ((0 <= 1) /\ (1 < 1))). We conclude that (~ (& 0 <= 1 < 1)). Qed.
imports: Coq.Reals.Reals Classical_Prop Automation Notations Tactics