proposition: Lemma zle_diffP a b: intp a -> intp b -> (a <=z b <-> inc (b -z a) BZp).
proof: Proof. pose aux a b := (a <=z b <-> inc (b -z a) BZp). move: a b. have Ha: (forall a b, inc a BZp -> inc b BZp -> aux a b). move => a b az bz. move: (BZp_sBZ bz) => bz1. move: (BZ_valN (BZp_sBZ az)) (BZ_valN bz1) => pa pb. rewrite /aux; apply: (iff_trans (zle_P1 az bz)). case: (equal_or_not a \0z) => anz. rewrite anz /BZdiff BZopp_0 BZsum_0r // BZ0_val;split => h //. apply:(cle0n pb). have az1: inc a BZps by apply /BZps_iP. move:(BZopp_positive1 az1) => az2;rewrite /BZdiff. move: (BZopp_val a)=> eq0. case: (cleT_el (CS_nat pa) (CS_nat pb)) => ce1. split; [move => _ | by done]. move: (BZsum_pm1 bz az2); rewrite eq0 => h; rewrite (h ce1). by apply: BZ_of_natp_i; apply: NS_diff. split; first by move/(cltNge ce1). move: (cdiff_nz ce1) => ne1. rewrite -eq0 in ce1; rewrite (BZsum_pm2 bz az2 ce1); rewrite eq0. rewrite /BZm_of_nat;Ytac0 => bad. by move:(BZp_sg bad);rewrite/int_pp;aw => ba;case:C0_ne_C1. have Hb: (forall a b, inc a BZ -> inc b BZp -> aux a b). move => a b pa pb;case /BZ_i0P: pa => ap; last by apply: Ha. split => _; first by apply: (ZpS_sum pb (BZps_sBZp (BZopp_negative1 ap))). exact (proj1 (zle_pr2 pb ap)). move => a b az bz. case /BZ_i0P: (bz) => bz1; last by apply: Hb. case /BZ_i0P: (az) => az1; last first. split; move => ha; first by case: (zle_pr4 az1 bz1). by move:(BZ_di_neg_pos (ZmsS_sum_l bz1 (BZopp_positive2 az1)) ha). move: (BZps_sBZp (BZopp_negative1 az1)) => tt. move: (Hb _ _ (ZSo bz) tt) => aux1. have ->: b -z a = (BZopp a -z BZopp b) by rewrite /BZdiff BZsumC (BZopp_K bz). split => ha. by move: (zle_opp ha); move /aux1. by move/aux1: ha => hb; move: (zle_opp hb); rewrite (BZopp_K az)(BZopp_K bz). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)