Deriving the Law of cosines c^2 = a^2 + b^2 - 2*a*b*cos(θ) in maxima

cosine-rule.mac

/*
You can run this file with

maxima -b cosine-rule.mac

or maybe also using M-x quickrun
*/

/*

Law of cosines - Wikipedia
https://en.wikipedia.org/wiki/Law_of_cosines

                  A
                  .
                 /|\-
               /- |  \
              /   |   \-
          c  /    |     \ b
            /     |h     \
           /      |       \-
         /-       |         \
        /         |        θ \-
       .----------+------------.
     B       x    a              C
*/

eq1: c^2 = x^2 + h^2;

eq2: b^2 = (a-x)^2 + h^2;

h2_in_eq1: subst(rhs(solve(eq2, h^2)[1]), h^2, eq1);

eq3: cos(θ) = (a-x)/b;

solve(eq3, x);

/* display2d:false; */

x_in_h2_in_eq1: subst(rhs(solve(eq3, x)[1]), x, h2_in_eq1), ratsimp;

/*

This arrives at the expected solution:

c^2 = a^2 + b^2 - 2*a*b*cos(θ)

or in pretty print:

         2    2    2
        c  = a  + b  - 2 a b cos(θ)

*/

output.txt

Maxima 5.47.0 https://maxima.sourceforge.io
using Lisp SBCL 2.3.11
Distributed under the GNU Public License. See the file COPYING.
Dedicated to the memory of William Schelter.
The function bug_report() provides bug reporting information.
(%i1) batch("qr_2QPK1V.mac")

read and interpret /tmp/qr_2QPK1V.mac
(%i2) eq1:c^2 = x^2+h^2
                                  2    2    2
(%o2)                            c  = x  + h
(%i3) eq2:b^2 = (a-x)^2+h^2
                               2          2    2
(%o3)                         b  = (a - x)  + h
(%i4) h2_in_eq1:subst(rhs(solve(eq2,h^2)[1]),h^2,eq1)
                              2            2    2
(%o4)                        c  = 2 a x + b  - a
(%i5) eq3:cos(θ) = (a-x)/b
                                         a - x
(%o5)                           cos(θ) = -----
                                           b
(%i6) solve(eq3,x)
(%o6)                         [x = a - b cos(θ)]
(%i7) ev(x_in_h2_in_eq1:subst(rhs(solve(eq3,x)[1]),x,h2_in_eq1),ratsimp)
                          2                     2    2
(%o7)                    c  = - 2 a b cos(θ) + b  + a
(%o9)                         /tmp/qr_2QPK1V.mac