proposition: Lemma sig_not_dec : forall P : Prop, {not (not P)} + {not P}.
proof: Proof. intros P. set (E := fun x => x = R0 \/ (x = R1 /\ P)). destruct (completeness E) as [x H]. - exists R1. intros x [->|[-> _]]. + apply Rle_0_1. + apply Rle_refl. - exists R0. now left. - destruct (Rle_lt_dec 1 x) as [H'|H']. + left. intros HP. elim Rle_not_lt with (1 := H'). apply Rle_lt_trans with (2 := Rlt_0_1). apply H. intros y [->|[_ Hy]]. * apply Rle_refl. * now elim HP. + right. intros HP. apply Rlt_not_le with (1 := H'). apply H. right. now split. Qed.
imports: RIneq