proposition: Lemma perm_right : forall x y z:U, cong (op (op x y) z) (op (op x z) y).
proof: 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_right; apply op_comm. + apply cong_sym; apply op_ass. Qed.