proposition: Theorem list_nth_rng_eq : ∀ α (r : ring α) la lb n, lap_eq la lb → (List.nth n la 0 = List.nth n lb 0)%K.
proof: Proof. intros α r la lb n Hlab. revert lb n Hlab. induction la as [| a]; intros. revert n. induction lb as [| b]; intros; [ reflexivity | simpl ]. apply lap_eq_nil_cons_inv in Hlab. destruct Hlab as (Hb, Hlb). symmetry in Hb. destruct n; [ assumption | idtac ]. rewrite <- IHlb; [ destruct n; reflexivity | assumption ]. revert n. induction lb as [| b]; intros. simpl. apply lap_eq_cons_nil_inv in Hlab. destruct Hlab as (Ha, Hla). destruct n; [ assumption | idtac ]. rewrite IHla; [ idtac | eassumption ]. destruct n; reflexivity. apply lap_eq_cons_inv in Hlab. destruct Hlab as (Hab, Hlab). destruct n; [ assumption | simpl ]. apply IHla; assumption. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation