proposition: Theorem R_sequence_dec : {forall n, P n} + {~ forall n, P n}.
proof: Proof. assert (H : {l f = 0} + {l f <> 0}). destruct (total_order_T (l f) 0) as [[Hlt|Heq]|Hgt]. right; apply Rlt_not_eq; assumption. left; assumption. right; apply Rgt_not_eq; assumption. destruct H as [H|H]. left; intros n. destruct (P_dec n) as [Hd|Hd]; [assumption|]. apply l_R0 with (n := n) in H. apply Heq2; assumption. right; intros Hneg; elim H. apply f_false; intros n. assert (Hd : {f n = false} + {f n <> false}). destruct (f n); [right|left]. intros Hc; discriminate Hc. reflexivity. destruct Hd as [Hd|Hd]; [assumption|]. apply Heq1 in Hd; elim Hd; apply Hneg. Qed.
imports: Reals Lia Lra