Explorando a janela CAS e provas matemáticas

Seria válido ou interessante, discutir CAS (cálculo algébrico simbólico), algo de álgebra booleana, elementos de lógica e provas matemáticas, em conjunto? Vejamos um exercício que propõe que se provem algumas propriedades de "produto interno" entre vetores do plano.