proposition: Theorem lap_eq_nil_lap_add_l : ∀ α (r : ring α) la lb, lap_eq [] lb → lap_eq la (lap_add la lb).
proof: Proof. intros α r la lb H. revert la. induction lb as [| b]; intros; [ destruct la; reflexivity | idtac ]. destruct la as [| a]; [ assumption | simpl ]. apply lap_eq_nil_cons_inv in H. destruct H as (Hb, Hlb). constructor; [ rewrite Hb, rng_add_0_r; reflexivity | idtac ]. apply IHlb; assumption. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation