proposition: Theorem series_order_iff {α} {R : ring α} {F : field R} : ∀ s n v, series_order s n = v ↔ match v with | fin k => (∀ i : nat, (i < k)%nat → (s .[n + i] = 0)%K) ∧ (s .[n + k] ≠ 0)%K | ∞ => ∀ i : nat, (s .[n + i] = 0)%K end.
proof: Proof. intros. split; intros H. subst v; unfold series_order. destruct (field_LPO (λ j : nat, s .[ n + j])) as [H1| (l, (H1, H2))]. assumption. split; assumption. unfold series_order. destruct (field_LPO (λ j : nat, s .[ n + j])) as [H1| (l, (H1, H2))]. destruct v as [k| ]; [ | apply eq_refl ]. destruct H as (H2, H3); exfalso; apply H3, H1. destruct v as [k| ]; [ | exfalso; apply H1, H ]. destruct H as (H3, H4). destruct (lt_eq_lt_dec k l) as [[H| H]| H]. exfalso; apply H4, H2, H. destruct H; apply eq_refl. exfalso; apply H1, H3, H. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series