proposition: Theorem first_such_that_has_prop : ∀ α (R : ring α) (K : field R) u n i k (P := (λ j, if fld_zerop (u j) then false else true)), (u (n + i)%nat ≠ 0)%K → k = first_such_that P n i → (u k ≠ 0)%K ∧ (∀ j : nat, (i ≤ j < k)%nat → (u j = 0)%K).
proof: Proof. intros α R K u n i k P Hn Hk. revert i k Hn Hk; induction n; intros. split; [ subst k; assumption | simpl ]. simpl in Hk; destruct Hk; intros j (H1, H2). apply lt_not_le in H2; exfalso; apply H2, H1. rewrite Nat.add_succ_l, <- Nat.add_succ_r in Hn. simpl in Hk; unfold P in Hk. destruct (fld_zerop (u i)) as [H1| H1]. pose proof IHn (S i) k Hn Hk as H2. destruct H2 as (H2, H3). split; [ apply H2 | intros j (H4, H5) ]. destruct (eq_nat_dec i j) as [H6| H6]; [ destruct H6; assumption | ]. apply H3; split; [ | assumption ]. apply Nat_le_neq_lt; assumption. destruct Hk; split; [ assumption | ]. intros j (H2, H3). apply lt_not_le in H3; exfalso; apply H3, H2. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series