proposition: Lemma ln1pc_in_int : forall x, { (0 <= x < 1)%R } + { ~(0 <= x < 1)%R }.
proof: Proof. intros x. destruct (Rle_dec 0 x) as [H1|H1]. destruct (Rlt_dec x 1) as [H2|H2]. left. now split. right. now contradict H2. right. now contradict H1. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)