proposition: Lemma ordinal_isomorphism_unique x y f: ordinalp x -> ordinalp y -> order_isomorphism f (ordinal_o x) (ordinal_o y) -> (x = y /\ f = identity x).
proof: Proof. move=> ox oy oif. move: (oif) => [_ _ [[[ff injf] [_ surf]] srcf trgf] pf]. rewrite !ordinal_o_sr in srcf trgf. have Wt: forall a, inc a x -> inc (Vf f a) y by move => a ax; Wtac. have prf2:forall a b, inc a x -> inc b x -> (inc a b <-> inc (Vf f a) (Vf f b)). move=> a b ax bx. apply: (iff_trans (iff_sym (ordo_ltP ox ax bx))). rewrite - srcf in ax bx. apply: (iff_trans (order_isomorphism_siso oif ax bx)). apply /ordo_ltP=> //; apply: Wt; ue. rewrite trgf srcf in surf. case:(all_exists_dichot1 (fun z => Vf f z = z) x) => H. suff xy: x = y by split => //; apply:identity_prop0=> //; split => //; ue. set_extens t => tx; first by rewrite - (H _ tx) - trgf; Wtac. by move: (surf _ tx)=> [z zx ->];rewrite (H _ zx). move: H =>[u ux up]. pose prop := fun z => inc z x /\ Vf f z <> z. have ppu: prop u by []. move: (least_ordinal1 (Os_ordinal ox ux) ppu). set z := least_ordinal _ _. move => [oz [zx fz] zle]. have p1: forall a, inc a z -> Vf f a = a. move=> a az; ex_middle aux. have ax:= (ordinal_transitive ox zx az). have aa:= (zle a (Os_ordinal oz az) (conj ax aux)). case: (ordinal_decent ox ax (aa _ az)). case: fz;case: (ordinal_inA (Os_ordinal oy (Wt _ zx)) oz). + rewrite srcf in injf; move => h. exact: (injf _ _ (ordinal_transitive ox zx h) zx (p1 _ h)). + move => ww. move:(surf _ (ordinal_transitive oy (Wt _ zx) ww)) => [a ax za]. by move: ww; rewrite {1 3} za => /(prf2 _ _ ax zx) /p1 ->. + done. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)