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