proposition: Lemma BZ_order_isomorphism_P f: (order_isomorphism f BZ_order BZ_order) <-> (exists2 u, intp u & f = Lf (fun z => z +z u) BZ BZ).
proof: Proof. pose p a := Lf (fun z => z +z a) BZ BZ. have Ha: forall a, intp a -> lf_axiom (fun z => z +z a) BZ BZ. by move => a az t tz; apply:ZSs. have Hb: forall a, intp a -> bijection (p a). move => a az; apply: lf_bijective; first by apply: Ha. by move => u v uz vz; apply:(BZsum_eq2r uz vz az). move => y ye; exists (y -z a); first by apply:ZS_diff. by rewrite BZsumC BZsum_diff. have Hc: forall a b c, intp a -> b <=z c -> (Vf (p a) b) <=z (Vf (p a) c). move => a b c az le1;move: (Ha _ az) => h; move: (le1) => [pa pb _]. by rewrite /p !LfV//; apply /(BZsum_le2r pa pb az). have Hd: (forall a, intp a -> order_isomorphism (p a)BZ_order BZ_order). move => a az. move: BZor_tor BZor_sr => to1 sor; move: (to1) => [or1 _]. have hh:{inc BZ &, fincr_prop (Lf (BZsum^~ a) BZ BZ) BZ_order BZ_order}. move => u v uz vz /= /zle_P cuv; apply /zle_P; apply: Hc az cuv. by apply:(total_order_isomorphism to1 or1 (Hb _ az)); rewrite /p; aw. split; last by move => [u uz ->]; apply: Hd. move => [_ _ [bf sf tf] incf]. move: sf tf; rewrite BZor_sr => sf tf. have He: (forall a b, a <=z b -> (Vf f a) <=z (Vf f b)). move => a b ab;move: (ab) => [pa pb _]; move:ab; move/zle_P. by rewrite /intp - sf in pa pb; move /(incf _ _ pa pb) /zle_P. have Hf: (forall a b, a <z b -> (Vf f a) <z (Vf f b)). move => a b [pa pb]; split; first by apply: He. dneg pc; move: (pa) => [xa xb _]; rewrite /intp - sf in xa xb. exact: (bij_inj bf xa xb pc). have Sa: forall x, intp x -> Vf f (BZsucc x) = (BZsucc (Vf f x)). rewrite /intp;move => x xz. have pa: inc (Vf f x) BZ by Wtac; fct_tac. move: (ZS_succ pa); rewrite /intp - tf => pb; move: (bij_surj bf pb) => [m]. rewrite sf;move => mf mv; suff: m = BZsucc x by move => <-. move: (Hf _ _ (zlt_succ xz)) => le1. case: (zleT_el mf (ZS_succ xz))=> le2; last first. move:(Hf _ _ le2); rewrite - mv; move /(zlt_succ1P (proj32_1 le1) pa). move => le3; BZo_tac. ex_middle ok; move /(zlt_succ1P mf xz): (conj le2 ok) => le3. move: (He _ _ le3); rewrite - mv => l1; move: (zlt_succ pa) => l2; BZo_tac. have Sb: forall x, intp x -> Vf f (BZpred x) = (BZpred (Vf f x)). move => x xz; move: (ZS_pred xz); rewrite /intp => pxz. rewrite -{2}(BZsucc_pred xz)(Sa _ pxz) BZpred_succ /intp // -tf;Wtac; fct_tac. have fz: inc (Vf f \0z) BZ by rewrite -tf;Wtac;[fct_tac |rewrite sf; apply:ZS0]. exists (Vf f \0z) => //. rewrite -/(p _); move: (Ha _ fz)(Hb _ fz); set g := p (Vf f \0z). move => Sc Sd. apply: function_exten; try fct_tac. by rewrite /g /p;aw. by rewrite /g /p;aw. rewrite sf;move => u usf /=. apply:(BZ_ind (p:= fun z => Vf f z = Vf g z)) => //. rewrite /g /p LfV//; [rewrite BZsum_0l // | apply: ZS0]. move => x xb; move: (ZS_succ xb) => sxb. by rewrite (Sa _ xb); move => ->;rewrite /g /p !LfV// (BZsucc_sum xb fz). move => x xb; move: (ZS_pred xb) => sxb. by rewrite (Sb _ xb); move => ->; rewrite /g /p ! LfV// (BZpred_sum xb fz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)