Group solver seems to work with version 0.9.11.2 of Idris. 3 aux lemmas to prove though