Basics: Rewritten the proof of test_mult1 using ssreflect.