はい、そういう検証もたいへん興味をそそられるのですが、
元の質問の動機は、スマリヤンの本の序盤のパズルを
覚えたてのcoqを電卓がわりに使って解けないかというぐらいのものなので、
ちょっと問題が大きい感じです。
hnfというtacticが標準であるので、
他の標準形にもちょいちょいと直せないものかと思った次第です。