The ::real is redundant---it is implied by the inequalities. So, the same bug is revealed by the simpler contrast of

is(a=b) assuming a^2=b^2, a>0, b>0;
is(a=b) assuming a^2=b^2, a>=0, b>=0;

I just point this out because it should make the bug easier to find/fix.

Now, given that Maple can correctly prove the second assertion above, shouldn't it be able to prove the following, which is much simpler (since it has half the number of variables) and is implied by the one above? Yet, it gets it wrong:

is(a=1) assuming a^2=1, a>=0;

     false

Weirder still, consider the negation of that assertion. One might guess that if Maple incorrectly answers false for an assertion, that it will answer true for the negation of that assertion. Yet

coulditbe(a <> 1) assuming a^2=1, a>=0;

     FAIL

The take-away from this is that it might be a good idea to also check the negation of an assertion. If one returns FAIL and the other doesn't, then the other can't be trusted.

@Kitonum Okay, you've changed my mind. I was thinking that the problem was in general too hard to be solved by an algorithm, but if Mathematica can do it, then Maple should be able to also.

@Mac Dude 

The with command is not needed to use a command in a module; any command in a module is accessible using :-. 

@Kitonum 

assume(n::posint);
limit(simplify(sin(convert(asympt(sqrt(n^2+n)*Pi, n, 1), polynom))^2), n= infinity);

     1

@tomleslie 

The Answer is satisfactory for me. In those cases where the sequence limit exists but the continuous doesn't, you need to use the positive integer property to do some sort of simplification. 

@Mac Dude The only significant difference between my original Answer and my update is an update to the second argument of subsindets, the one that selects the subexpressions by their type. In the Answer, this is specfunc({sum,Sum}), which selects any function whose name is sum or Sum. This is updated to 

And(specfunc({sum,Sum}), patfunc(`+`, anything))

which selects any functions whose name is sum or Sum And whose first argument is type `+` and whose remaining argument(s) can be anything.

@Mac Dude 

A problem with your DistSum is that it requires the overall expression to be of the specified type rather than looking for subexpressions of the specified type. Thus it won't work on your original example, which, indeed, isn't a sum or Sum. So, the thing to do is to fine tune the second argument to subsindets, which determines which subexpressions to work on. Here it is:

DistSum:= (xpr)->
     subsindets[flat](
          xpr,
          And(specfunc({sum,Sum}), patfunc(`+`, anything)),
          S-> map(op(0,S), op(S))
     )
:

Things like specfunc and patfunc are documented on the page ?type,structured---an extremely dense help page that I've been studying for years. I find it strange that with all the options on that page, there's not one that combines this use of specfunc and patfunc. Well, at least there's not one that I could spot. I can't figure them all out just from the documentation.

@MDD 

Okay, I'm glad that you already understand some of it. That means I can move faster through this. Let's consider the next line:

S:= solve({coeffs(expand(`+`((C*~L)[])), V)}, C),

especially the part at its heart, `+`((C*~L)[]).

Your question gave me the impression that you thought that the C* and the ~ were separate operations. No: The ~ preceded by almost any other binary operator makes the operator an elementwise operator (see ?elementwise). So C*~L multiplies the coefficients by the polynomials and produces a new list or set (it doesn't matter which in this case) containing the products.

Appending [] to a set or list extracts its underlying sequence of elements. Passing these to `+` adds them. So `+`((C*~L)[]) computes the dot product of C and L. The rest of the line expands this polynomial, extracts its coefficients with respect to V, sets them to 0, and solves this linear system for the variables C. The final result of this is a set S of the form

{c[1]=..., c[2]=..., ..., c[n]=...}.

Note that it's a homogenous and square linear system, so it always has a solution, which solve always finds.

Now let's consider the next line

F:= indets(rhs~(S), name) intersect C=~ 1;

First consider the rhs~(S). This applies rhs to every element of S, producing a new set containing just the right-hand sides of the equations in S. All the names in this set are extracted. This represents the free variables in the solution set S, which is why I call it F. From these free variables, I only want the linear coefficients, not the parameters; so, I intersect with C. 

Then I want to equate all these free variables to 1. My choice of 1 is arbitrary; I could use any nonzero value, because I want to return, if possible, a definite but nontrivial solution to the homogenous linear system. The elementwise operation A =~ 1 forms with every member of A an equation whose right side is 1. So the final result of this line is a set F of the form

{c[a]=1, c[b]=1, ...},

where the c[a], c[b], etc., represent only the free variables in S that are also in C.

Now let's consider the last line of CoeffsOfLinComb, which forms the return value:

eval([C[]], eval(S,F) union F) .

This takes the set C, forms the corresponding list [C[]], and evaluates each of these using 1 for all the free linear coefficients. The final result is a list of length nops(L) that contains only numbers and parameters.

Now let's consider the next procedure, PolyLinearCombo, and its first executable line

C:= CoeffsOfLinComb([f, F[]], V);

This takes the target polynomial f, makes it the first element of a list [f, F[]] and finds the linear coefficients, if any, that are needed to produce 0.

The final line is 

if C[1]=0 then (false, []) else (true, -C[2..] /~ C[1]) end if.

If the coefficient of f is 0, then f is linearly independent of F. Otherwise, the dependency coefficients are the coefficients of F divided by the negative of the coefficient of f. The elementwise operator /~ performs the division on all the other coefficients. The C[2..] means the sublist of C starting with the second element and going to the end.

@mattcanderson1 

It is ambiguous whether the OP is interested in the convergence/divergence of a series or of a sequence. Since the word "series" is used and "sequence" isn't, I think that a series is more likely. But then there's "Is this function convergent or divergent?", which implies an interest in the sequence.
 

@MDD There's a lot to explain. I may do this a few lines at a time. I'll start with procedure CoeffsOfLinComb, which is my version of Kitonum's algorithm. I guess that the first line that needs some explanation is 

  V::set(name):= indets(L, And(name, Not(constant))).

This declares the second parameter to be called V. If a corresponding second argument is passed, it must be a set of names; if a second argument isn't passed, then V will be assigned a default value of all the names in the first argument, L, that are Not constants (such as Pi).

The next thing that might need explaining is 

C:= {c[k] $ k= 1..nops(L)}.

This declares a local variable C and assigns it the value of a set {c[1], c[2], ..., c[n]} where n is the number of polynomials in L (nops(L)). This can be expressed (with the $ sequencing operator) as "the set of c[k] where k runs from 1 to nops(L)."

I'm tired...that's enough for now.

@Kanellopoulos I don't know if the Maple is correct. There is that 1 point (out of the 18 that I checked) with relatively high residuals. Can you check the residuals in Mathematica? 

Maple's algorithm is the "theta method". This is the only method that it ever uses when there's more than one PDE.

@Kanellopoulos It's a moot point now because I've already reconstructed your worksheet by cut-and-paste from the PDF, but please, next time, upload the worksheet directly to MaplePrimes using the green up arrow like I said. The Dropbox version is unusable to me.

We can read the PDFs, but not work with them in Maple. Use the green up arrow on the toolbar in the MaplePrimes editor (last item on the second row of the toolbar) to upload a Maple worksheet in .mw or .mws format.

Please post the equations, the Maple code that you used to solve them, and the Maple code that you used to plot. Regarding checking the solution: That is generally possible through numeric differentiation with the fdiff command.

@MDD It's done. Please find procedure PolyLinearCombo in an Answer below.