小编And*_*sky的帖子

假设我们试图形式化一些(半)组理论属性,如下所示:

Section Group.

Variable A: Type.
Variable op: A -> A -> A.

Definition is_left_neutral  (e: A) := forall x: A, (op e x) = x.
Definition is_right_neutral (e: A) := forall x: A, x = (op x e).

Lemma uniqueness_of_neutral:
  forall a b: A, (is_left_neutral a) -> (is_right_neutral b) -> (a = b).
Proof.
  intro; intro.
  intros lna rnb.
  elim lna with b; elim rnb with a.
  reflexivity.
Qed.

End Group.

它的工作正常,但是,如果我们在上述任一定义中反转方程式,即将定义替换为

Definition is_left_neutral  (e: A) := …