(proof-new) proofs for arith-constraint explanations (#5224)

(proof-new) proofs for arith-constraint explanations (#5224)

Threads proofs through arith::Constraint's machinery for explaining
constraints. Changes, by function:

externalExplainByAssertions:
introduce scope to prove the implication
externalExplainForPropagation:
introduce scope to prove the implication
externalExplainConflict:
use other machinery to prove conflicting constraints
use the CONTRA rule
introduce scope to close the conflict proof
Future commits will pick up these proofs in theory_arith_private.cpp.
Future commits will prove the "split" lemmas produced in constraint.cpp