Permut.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* G. Huet 1-9-95 *)

We consider a Set U, given with a commutative-associative operator op, and a congruence cong; we show permutation lemmas

Section Axiomatisation.

  Variable U : Type.
  Variable op : U -> U -> U.
  Variable cong : U -> U -> Prop.

  Hypothesis op_comm : forall x y:U, cong (op x y) (op y x).
  Hypothesis op_ass : forall x y z:U, cong (op (op x y) z) (op x (op y z)).

  Hypothesis cong_left : forall x y z:U, cong x y -> cong (op x z) (op y z).
  Hypothesis cong_right : forall x y z:U, cong x y -> cong (op z x) (op z y).
  Hypothesis cong_trans : forall x y z:U, cong x y -> cong y z -> cong x z.
  Hypothesis cong_sym : forall x y:U, cong x y -> cong y x.

Remark. we do not need: Hypothesis cong_refl : (x:U)(cong x x).

  Lemma cong_congr :
    forall x y z t:U, cong x y -> cong z t -> cong (op x z) (op y t).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x y : U, cong (op x y) (op y x)
op_ass:forall x y z : U,
cong (op (op x y) z) (op x (op y z))
cong_left:forall x y z : U,
cong x y -> cong (op x z) (op y z)
cong_right:forall x y z : U,
cong x y -> cong (op z x) (op z y)
cong_trans:forall x y z : U,
cong x y -> cong y z -> cong x z
cong_sym:forall x y : U, cong x y -> cong y x
forall x y z t : U,
cong x y -> cong z t -> cong (op x z) (op y t)
  Proof.U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x y : U, cong (op x y) (op y x)
op_ass:forall x y z : U,
cong (op (op x y) z) (op x (op y z))
cong_left:forall x y z : U,
cong x y -> cong (op x z) (op y z)
cong_right:forall x y z : U,
cong x y -> cong (op z x) (op z y)
cong_trans:forall x y z : U,
cong x y -> cong y z -> cong x z
cong_sym:forall x y : U, cong x y -> cong y x
forall x y z t : U,
cong x y -> cong z t -> cong (op x z) (op y t)
    intros; apply cong_trans with (op y z).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
H:cong x y
H0:cong z t
cong (op x z) (op y z)
U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
H:cong x y
H0:cong z t
cong (op y z) (op y t)
    -U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
H:cong x y
H0:cong z t
cong (op x z) (op y z) apply cong_left; trivial.
    -U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
H:cong x y
H0:cong z t
cong (op y z) (op y t) apply cong_right; trivial.
  Qed.

  Lemma comm_right : forall x y z:U, cong (op x (op y z)) (op x (op z y)).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x y : U, cong (op x y) (op y x)
op_ass:forall x y z : U,
cong (op (op x y) z) (op x (op y z))
cong_left:forall x y z : U,
cong x y -> cong (op x z) (op y z)
cong_right:forall x y z : U,
cong x y -> cong (op z x) (op z y)
cong_trans:forall x y z : U,
cong x y -> cong y z -> cong x z
cong_sym:forall x y : U, cong x y -> cong y x
forall x y z : U, cong (op x (op y z)) (op x (op z y))
  Proof.U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x y : U, cong (op x y) (op y x)
op_ass:forall x y z : U,
cong (op (op x y) z) (op x (op y z))
cong_left:forall x y z : U,
cong x y -> cong (op x z) (op y z)
cong_right:forall x y z : U,
cong x y -> cong (op z x) (op z y)
cong_trans:forall x y z : U,
cong x y -> cong y z -> cong x z
cong_sym:forall x y : U, cong x y -> cong y x
forall x y z : U, cong (op x (op y z)) (op x (op z y))
    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).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x y : U, cong (op x y) (op y x)
op_ass:forall x y z : U,
cong (op (op x y) z) (op x (op y z))
cong_left:forall x y z : U,
cong x y -> cong (op x z) (op y z)
cong_right:forall x y z : U,
cong x y -> cong (op z x) (op z y)
cong_trans:forall x y z : U,
cong x y -> cong y z -> cong x z
cong_sym:forall x y : U, cong x y -> cong y x
forall x y z : U, cong (op (op x y) z) (op (op y x) z)
  Proof.U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x y : U, cong (op x y) (op y x)
op_ass:forall x y z : U,
cong (op (op x y) z) (op x (op y z))
cong_left:forall x y z : U,
cong x y -> cong (op x z) (op y z)
cong_right:forall x y z : U,
cong x y -> cong (op z x) (op z y)
cong_trans:forall x y z : U,
cong x y -> cong y z -> cong x z
cong_sym:forall x y : U, cong x y -> cong y x
forall x y z : U, cong (op (op x y) z) (op (op y x) z)
    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).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x y : U, cong (op x y) (op y x)
op_ass:forall x y z : U,
cong (op (op x y) z) (op x (op y z))
cong_left:forall x y z : U,
cong x y -> cong (op x z) (op y z)
cong_right:forall x y z : U,
cong x y -> cong (op z x) (op z y)
cong_trans:forall x y z : U,
cong x y -> cong y z -> cong x z
cong_sym:forall x y : U, cong x y -> cong y x
forall x y z : U, cong (op (op x y) z) (op (op x z) y)
  Proof.U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x y : U, cong (op x y) (op y x)
op_ass:forall x y z : U,
cong (op (op x y) z) (op x (op y z))
cong_left:forall x y z : U,
cong x y -> cong (op x z) (op y z)
cong_right:forall x y z : U,
cong x y -> cong (op z x) (op z y)
cong_trans:forall x y z : U,
cong x y -> cong y z -> cong x z
cong_sym:forall x y : U, cong x y -> cong y x
forall x y z : U, cong (op (op x y) z) (op (op x z) y)
    intros.U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op (op x y) z) (op (op x z) y)
    apply cong_trans with (op x (op y z)).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op (op x y) z) (op x (op y z))
U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op x (op y z)) (op (op x z) y)
    -U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op (op x y) z) (op x (op y z)) apply op_ass.
    -U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op x (op y z)) (op (op x z) y) apply cong_trans with (op x (op z y)).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op x (op y z)) (op x (op z y))
U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op x (op z y)) (op (op x z) y)
      +U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op x (op y z)) (op x (op z y)) apply cong_right; apply op_comm.
      +U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op x (op z y)) (op (op x z) y) apply cong_sym; apply op_ass.
  Qed.

  Lemma perm_left : forall x y z:U, cong (op x (op y z)) (op y (op x z)).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x y : U, cong (op x y) (op y x)
op_ass:forall x y z : U,
cong (op (op x y) z) (op x (op y z))
cong_left:forall x y z : U,
cong x y -> cong (op x z) (op y z)
cong_right:forall x y z : U,
cong x y -> cong (op z x) (op z y)
cong_trans:forall x y z : U,
cong x y -> cong y z -> cong x z
cong_sym:forall x y : U, cong x y -> cong y x
forall x y z : U, cong (op x (op y z)) (op y (op x z))
  Proof.U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x y : U, cong (op x y) (op y x)
op_ass:forall x y z : U,
cong (op (op x y) z) (op x (op y z))
cong_left:forall x y z : U,
cong x y -> cong (op x z) (op y z)
cong_right:forall x y z : U,
cong x y -> cong (op z x) (op z y)
cong_trans:forall x y z : U,
cong x y -> cong y z -> cong x z
cong_sym:forall x y : U, cong x y -> cong y x
forall x y z : U, cong (op x (op y z)) (op y (op x z))
    intros.U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op x (op y z)) (op y (op x z))
    apply cong_trans with (op (op x y) z).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op x (op y z)) (op (op x y) z)
U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op (op x y) z) (op y (op x z))
    -U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op x (op y z)) (op (op x y) z) apply cong_sym; apply op_ass.
    -U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op (op x y) z) (op y (op x z)) apply cong_trans with (op (op y x) z).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op (op x y) z) (op (op y x) z)
U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op (op y x) z) (op y (op x z))
      +U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op (op x y) z) (op (op y x) z) apply cong_left; apply op_comm.
      +U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z:U
cong (op (op y x) z) (op y (op x z)) apply op_ass.
  Qed.

  Lemma op_rotate : forall x y z t:U, cong (op x (op y z)) (op z (op x y)).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x y : U, cong (op x y) (op y x)
op_ass:forall x y z : U,
cong (op (op x y) z) (op x (op y z))
cong_left:forall x y z : U,
cong x y -> cong (op x z) (op y z)
cong_right:forall x y z : U,
cong x y -> cong (op z x) (op z y)
cong_trans:forall x y z : U,
cong x y -> cong y z -> cong x z
cong_sym:forall x y : U, cong x y -> cong y x
forall x y z : U,
U -> cong (op x (op y z)) (op z (op x y))
  Proof.U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x y : U, cong (op x y) (op y x)
op_ass:forall x y z : U,
cong (op (op x y) z) (op x (op y z))
cong_left:forall x y z : U,
cong x y -> cong (op x z) (op y z)
cong_right:forall x y z : U,
cong x y -> cong (op z x) (op z y)
cong_trans:forall x y z : U,
cong x y -> cong y z -> cong x z
cong_sym:forall x y : U, cong x y -> cong y x
forall x y z : U,
U -> cong (op x (op y z)) (op z (op x y))
    intros; apply cong_trans with (op (op x y) z).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
cong (op x (op y z)) (op (op x y) z)
U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
cong (op (op x y) z) (op z (op x y))
    -U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
cong (op x (op y z)) (op (op x y) z) apply cong_sym; apply op_ass.
    -U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
cong (op (op x y) z) (op z (op x y)) apply op_comm.
  Qed.

Needed for treesort ...

  Lemma twist :
    forall x y z t:U, cong (op x (op (op y z) t)) (op (op y (op x t)) z).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x y : U, cong (op x y) (op y x)
op_ass:forall x y z : U,
cong (op (op x y) z) (op x (op y z))
cong_left:forall x y z : U,
cong x y -> cong (op x z) (op y z)
cong_right:forall x y z : U,
cong x y -> cong (op z x) (op z y)
cong_trans:forall x y z : U,
cong x y -> cong y z -> cong x z
cong_sym:forall x y : U, cong x y -> cong y x
forall x y z t : U,
cong (op x (op (op y z) t)) (op (op y (op x t)) z)
  Proof.U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x y : U, cong (op x y) (op y x)
op_ass:forall x y z : U,
cong (op (op x y) z) (op x (op y z))
cong_left:forall x y z : U,
cong x y -> cong (op x z) (op y z)
cong_right:forall x y z : U,
cong x y -> cong (op z x) (op z y)
cong_trans:forall x y z : U,
cong x y -> cong y z -> cong x z
cong_sym:forall x y : U, cong x y -> cong y x
forall x y z t : U,
cong (op x (op (op y z) t)) (op (op y (op x t)) z)
    intros.U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
cong (op x (op (op y z) t)) (op (op y (op x t)) z)
    apply cong_trans with (op x (op (op y t) z)).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
cong (op x (op (op y z) t)) (op x (op (op y t) z))
U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
cong (op x (op (op y t) z)) (op (op y (op x t)) z)
    -U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
cong (op x (op (op y z) t)) (op x (op (op y t) z)) apply cong_right; apply perm_right.
    -U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
cong (op x (op (op y t) z)) (op (op y (op x t)) z) apply cong_trans with (op (op x (op y t)) z).U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
cong (op x (op (op y t) z)) (op (op x (op y t)) z)
U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
cong (op (op x (op y t)) z) (op (op y (op x t)) z)
      +U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
cong (op x (op (op y t) z)) (op (op x (op y t)) z) apply cong_sym; apply op_ass.
      +U:Type
op:U -> U -> U
cong:U -> U -> Prop
op_comm:forall x0 y0 : U, cong (op x0 y0) (op y0 x0)
op_ass:forall x0 y0 z0 : U,
cong (op (op x0 y0) z0) (op x0 (op y0 z0))
cong_left:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op x0 z0) (op y0 z0)
cong_right:forall x0 y0 z0 : U,
cong x0 y0 -> cong (op z0 x0) (op z0 y0)
cong_trans:forall x0 y0 z0 : U,
cong x0 y0 -> cong y0 z0 -> cong x0 z0
cong_sym:forall x0 y0 : U, cong x0 y0 -> cong y0 x0
x, y, z, t:U
cong (op (op x (op y t)) z) (op (op y (op x t)) z) apply cong_left; apply perm_left.
  Qed.

End Axiomatisation.