proposition: Theorem field_LPO : ∀ α (R : ring α) (K : field R) (u : nat -> α), (∀ i, (u i = 0)%K) + { i | (u i ≠ 0)%K ∧ ∀ j, (j < i)%nat → (u j = 0)%K }.
proof: Proof. intros. pose proof (LPO (λ i, if fld_zerop (u i) then O else S O)) as H. destruct H as [H| H]. left; intros i. pose proof H i as Hi. destruct (fld_zerop (u i)); [ assumption | discriminate Hi ]. right. destruct H as (i, Hi). destruct (fld_zerop (u i)) as [| H]; [ exfalso; apply Hi, eq_refl | ]. clear Hi. set (P j := if fld_zerop (u j) then false else true). remember (first_such_that P i O) as m eqn:Hm. exists m. replace i with (i + O)%nat in H by (rewrite Nat.add_0_r; apply eq_refl). pose proof @first_such_that_has_prop α R K u i 0 m H Hm as H1. destruct H1 as (H1, H2). split; [ assumption | intros j Hj ]. apply H2. split; [ apply Nat.le_0_l | assumption ]. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series