proposition: Lemma perm_left : forall x y z:U, cong (op x (op y z)) (op y (op x z)).
proof: Proof. intros. apply cong_trans with (op (op x y) z). - apply cong_sym; apply op_ass. - apply cong_trans with (op (op y x) z). + apply cong_left; apply op_comm. + apply op_ass. Qed.