Coq演習 - memo

Lemma inv_r : forall x, x * / x = 1.
Proof.
  intros.
  assert(H: //x/x=1).
  rewrite inv_l. reflexivity.
(*

1 subgoals, subgoal 1 (ID 150)
  
  x : G
  H : / / x / x = 1
  ============================
   x / x = 1
 ここで、//x = xが示せれば、証明終わりなんだろうけど・・・
 上手くいかない。

  方針から間違ってるのか
 *)
Admitted.

数学やっぱ向いてないわ。

githubにリポジトリを作ってみた。
https://github.com/moritanon/Coq2014.git
早速挫折しそうだが。