proposition: Theorem lap_eq_app_0s : ∀ α (r : ring α) la lb, List.Forall (λ b, b = 0)%K lb → lap_eq la (la ++ lb).
proof: Proof. intros α r la lb Hz. induction la as [| a]; simpl. induction lb as [| b]; [ reflexivity | idtac ]. constructor. apply list_Forall_inv in Hz; destruct Hz; assumption. apply IHlb. apply list_Forall_inv in Hz; destruct Hz; assumption. constructor; [ reflexivity | assumption ]. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation