proposition: Lemma BZ_order_props_bis r: nonempty (substrate r) -> or_likeZ r -> r \Is BZ_order.
proof: Proof. move => [u uE] [pa pb pc]; apply: orderIS. pose fp := induction_term (fun _ v => (or_succ r v)) u. pose fn := induction_term (fun _ v => (or_pred r v)) u. have ra: fp \0c = u by apply: (induction_term0). have rb: fn \0c = u by apply: (induction_term0). have rc: forall n, natp n -> fp (csucc n) = (or_succ r (fp n)). apply:induction_terms. have rd: forall n, natp n -> fn (csucc n) = (or_pred r (fn n)). apply:induction_terms. have re: forall n, natp n -> inc (fp n) (substrate r). apply: Nat_induction; [ ue | move => n nN Hrec]. move: (proj1 (or_succ_prop pa (proj1 (pb _ Hrec)))); rewrite - (rc _ nN). move => aux; order_tac. have rf: forall n, natp n -> inc (fn n) (substrate r). apply: Nat_induction; [ ue | move => n nN Hrec]. move: (proj1 (or_pred_prop pa (proj2 (pb _ Hrec)))); rewrite - (rd _ nN). move => aux; order_tac. have rg: forall n, natp n -> consecutive r (fp n) (fp (csucc n)). move => n nN; rewrite (rc _ nN); apply: (or_succ_prop pa). exact:(proj1 (pb _ (re _ nN))). have rh: forall n, natp n -> consecutive r (fn (csucc n)) (fn n). move => n nN; rewrite (rd _ nN); apply: (or_pred_prop pa). exact:(proj2 (pb _ (rf _ nN))). have spa: forall z, inc z BZp -> BZsucc z = BZ_of_nat (csucc (BZ_val z)). move => z zp; move: (BZps_sBZp ZpsS1) CS0=> aa cs0. rewrite /BZsucc BZsumE /BZsum_v2 (Y_true (conj zp aa)). rewrite (Nsucc_rw (BZ_valN (BZp_sBZ zp))) //. by rewrite /BZ_one BZ_of_nat_val. have spb: forall z, inc z BZms -> BZpred z = BZm_of_nat (csucc (BZ_val z)). move => z zp. move: (BZ_di_neg_pos zp) (BZ_di_neg_pos ZmsS_m1) => ha hb. rewrite /BZpred /BZdiff BZopp_1 /BZ_mone BZsumE /BZsum_v2. have hc: ~(inc z BZp /\ inc (BZm_of_nat \1c) BZp) by case. rewrite (Y_false hc) (Y_true (conj ha hb)). by rewrite BZm_of_nat_val (Nsucc_rw (BZ_valN (BZms_sBZ zp))). pose fc x := Yo (Q x = C0) (fn (P x)) (fp (P x)). set f := Lf fc BZ (substrate r). have qa: forall z, intp z -> inc (fc z) (substrate r). move => z /BZ_valN h; rewrite /fc; Ytac hh; fprops. have ff: function f by apply: lf_function. have sf: source f = BZ by rewrite /f; aw. have tf: target f = substrate r by rewrite /f; aw. have z0 := ZS0; have z1 := ZS1. have spc: forall z, intp z -> consecutive r (Vf f z) (Vf f (BZsucc z)). move => z zz; move:(ZS_succ zz) => zz'; rewrite /f !LfV//. case /BZ_i0P: (zz) => zp; last first. rewrite (spa _ zp) /fc (BZp_sg zp) (BZ_of_nat_val) /BZ_of_nat; aw. Ytac0; Ytac0; exact: (rg _ (BZ_valN zz)). case: (equal_or_not z \1mz) => zm1. rewrite zm1 /BZsucc -{2} BZopp_1 (BZsum_opp_l ZS1) /fc. rewrite (BZp_sg ZpS0) (BZms_sg ZmsS_m1); Ytac0; Ytac0. rewrite BZ_of_nat_val BZm_of_nat_val - succ_zero. by move:(rh _ NS0); rewrite ra rb. have sbn: inc (BZsucc z) BZms. apply /zgt0xP; split; first by apply /zlt_succ2P => //; apply /zgt0xP. by dneg sa; rewrite - (BZpred_succ zz) sa /BZpred - BZopp_1 BZdiff_0l. rewrite /fc (BZms_sg zp) (BZms_sg sbn); Ytac0; Ytac0. rewrite - {1} (BZpred_succ zz) (spb _ sbn) BZm_of_nat_val. exact: (rh _ (BZ_valN (BZms_sBZ sbn))). move: (Imf_P ff); rewrite {1} sf => iP. have qd: or_stable r (Imf f). move => x /iP [v vz ->]; split. rewrite - (or_succ_prop' pa (spc _ vz)); apply /iP. exists (BZsucc v) => //; apply: (ZS_succ vz). rewrite -(BZsucc_pred vz) - (or_pred_prop' pa (spc _ (ZS_pred vz))). apply /iP; exists (BZpred v) => //;apply: (ZS_pred vz). move: (Imf_Starget ff); rewrite {2}/f; aw => qe. case: (pc _ qe qd) => ip. by empty_tac1 (Vf f \0z); apply /iP; exists \0z. move: (proj1 BZor_tor) (proj1 pa) => or1 or2. have [_ _ _ sif]:strict_increasing_fun f BZ_order r. by apply:BZ_order_sfinc => // z /spc []. have bf: bijection_prop f (substrate BZ_order) (substrate r). hnf; rewrite BZor_sr sf - ip {2} /f; aw; split => //. split; last by apply: (surjective_pr1 ff); rewrite {2}/f; aw. by split => //; rewrite sf => a b af bf h; case: (zleT_ell af bf) => //; move /zlt_P /sif => []_; rewrite h. exists f; split => //. hnf; rewrite sf => a b az bz; split. move /zle_P => laz; case: (equal_or_not a b) => eq. rewrite eq; order_tac; Wtac. by move /zlt_P: (conj laz eq) => /sif []. move => h; apply /zle_P; case: (zleT_el az bz) => // /zlt_P /sif ha;order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)