Coqで証明

使用言語　Coq
反対称関係において最大限が存在すれば一意

Example hantaisyo U R:=
forall a b:U,R a b->R b a->a=b:Prop.

Example saidaigen U(R:U->U->Prop)a:=
forall x,R x a.

Goal forall U(R:U->U->Prop)a b,
hantaisyo U R->
saidaigen U R a->
saidaigen U R b->
a=b.
Proof.
intros.
unfold hantaisyo in H.
specialize(H a b).
unfold saidaigen in H0.
unfold saidaigen in H1.
specialize(H0 b).
specialize(H1 a).
specialize(H H1 H0).
clear H0 H1 R.
case H.
clear b H.
reflexivity.
Qed.