proposition: Theorem list_nth_lap_eq : ∀ α (r : ring α) la lb, (∀ i, (List.nth i la 0 = List.nth i lb 0)%K) → lap_eq la lb.
proof: Proof. intros α r la lb Hi. revert lb Hi. induction la as [| a]; intros. induction lb as [| b]; [ reflexivity | constructor ]. pose proof (Hi O) as H. symmetry; assumption. apply IHlb; intros i. pose proof (Hi (S i)) as H; simpl in H; rewrite <- H. destruct i; reflexivity. induction lb as [| b]. constructor. pose proof (Hi O) as H. assumption. apply IHla; intros i. pose proof (Hi (S i)) as H; simpl in H; rewrite H. destruct i; reflexivity. constructor. pose proof (Hi O) as H. assumption. apply IHla; intros i. pose proof (Hi (S i)) as H. assumption. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation