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が示せれば、証明終わりなん…

仕事の現場がまた変わるらしい。なんで私だけなのか。 文句ばっかり言ってたから外されたのかしら。その仕事自体がぽしゃったっぽい。 今の仕事楽だからいいんだけど、あまり長くいたくない。腐りそうだし。