check with Agda-2.4.2.1 and agda-stdlib-0.9
remove distrib-²-* and use SemiringSolver instead
use _$_ to pass equational reasoning proofs directly to functions
flatten pattern matches in the definition of a²mod3≡0