It would seem that someone has done this but my search says "No" My First two attempts failed:
Clear[{c, a, b, \[Theta]}];
FindEquationalProof[c\[LessEqual]a+b,{c^2==a^2-2*a*b*Cos[\[Theta]]+\
b^2,a^2+2*a*b*Cos[\[Theta]]+b^2==(a+b)^2}]
and
FindEquationalProof[c <= a + b, c^2 == a^2 + b^2]
I realize Mathematica needs to know that ABC is a triangle, but have not come up with a way to provide that assumption other than numerically.
