diff options
Diffstat (limited to 'theories/Sets/Permut.v')
| -rw-r--r-- | theories/Sets/Permut.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/theories/Sets/Permut.v b/theories/Sets/Permut.v index 6c9a064c1..f593031a0 100644 --- a/theories/Sets/Permut.v +++ b/theories/Sets/Permut.v @@ -36,23 +36,23 @@ Section Axiomatisation. apply cong_left; trivial. apply cong_right; trivial. Qed. - + Lemma comm_right : forall x y z:U, cong (op x (op y z)) (op x (op z y)). Proof. intros; apply cong_right; apply op_comm. Qed. - + Lemma comm_left : forall x y z:U, cong (op (op x y) z) (op (op y x) z). Proof. intros; apply cong_left; apply op_comm. Qed. - + Lemma perm_right : forall x y z:U, cong (op (op x y) z) (op (op x z) y). Proof. intros. apply cong_trans with (op x (op y z)). apply op_ass. - apply cong_trans with (op x (op z y)). + apply cong_trans with (op x (op z y)). apply cong_right; apply op_comm. apply cong_sym; apply op_ass. Qed. @@ -66,7 +66,7 @@ Section Axiomatisation. apply cong_left; apply op_comm. apply op_ass. Qed. - + Lemma op_rotate : forall x y z t:U, cong (op x (op y z)) (op z (op x y)). Proof. intros; apply cong_trans with (op (op x y) z). |