[Coq][Math] From left unit and left inverse to right unit and inverse

群で左単位元と左逆元があれば、右単位元と右逆元があることの説明。

Coq 演習で、Coq 以外のところで行き詰まっていた人がいたので参考になればと。

逆元と単位元の導入/除去のとこだけ詳しく書きますが、結合則使って演算順序を変えるところは各自 rewrite とかで頑張ってください。

$x 1 = 1 x 1 = \{(x^{-1})^{-1} x^{-1}\} x (x^{-1}x) = (x^{-1})^{-1} (x^{-1}x) x^{-1}x $
$ = (x^{-1})^{-1} 1 x^{-1} x = (x^{-1})^{-1} x^{-1} x = \{ (x^{-1})^{-1} x^{-1}\} x = 1 x = x$

$x x^{-1} = 1 x x^{-1} = \{ (x^{-1})^{-1} x^{-1} \} x x^{-1} $
$= (x^{-1})^{-1} (x^{-1}x) x^{-1} = (x^{-1})^{-1}  1  x^{-1}$
$= (x^{-1})^{-1} (1 x^{-1}) = (x^{-1})^{-1} x^{-1} = 1 $