proposition: Lemma zle_triangular n m: intp n -> intp m -> (BZabs (n +z m)) <=z (BZabs n) +z (BZabs m).
proof: Proof. move: n m. pose aux n m := BZabs (n +z m) <=z BZabs n +z BZabs m. suff: forall n m, inc n BZp -> intp m -> aux n m. move => h n m; case /BZ_i0P; last by apply: h. move => pa pb; rewrite - (BZabs_opp) - (BZabs_opp n)- (BZabs_opp m). rewrite (BZoppD (BZms_sBZ pa) pb); apply: h; last by apply: (ZSo pb). apply:(BZopp_negative2 (BZms_sBZm pa)). move => n m np; case /BZ_i0P; last first. move => mp; rewrite /aux (BZabs_pos np) (BZabs_pos mp). move:(ZpS_sum np mp) => pa; move: (BZp_sBZ pa) => pb. rewrite (BZabs_pos pa); apply: (zleR pb). move => mn. move: (BZp_sBZ np) (BZms_sBZ mn) => nz mz. move: (BZ_valN nz) (BZ_valN mz) => pn pm. rewrite /aux (BZabs_pos np) (BZabs_neg mn). have [re1 _]: n<z n +z BZopp m. by move: (BZsum_Mps nz (BZopp_negative1 mn)). have re2: BZopp m <=z n +z BZopp m. rewrite BZsumC; exact(BZsum_Mp (ZSo mz) np). case: (cleT_el (CS_nat pm) (CS_nat pn)) => ce1. rewrite (BZsum_pm1 np mn ce1); move: (cdiff_ab_le_a (P m) (CS_nat pn)). set k := P n -c P m => ce2; rewrite /BZabs /BZ_of_nat; aw. have kz: inc (J k C1) BZp by apply: indexed_pi => //;apply: NS_diff. have le2: P (J k C1) <=c P n by aw. move/ (zle_P1 kz np): le2 => le3; BZo_tac. rewrite (BZsum_pm2 np mn ce1); move: (cdiff_ab_le_a (P n) (CS_nat pm)). move: (cdiff_nz ce1); set k := P m -c P n => knz ce2. rewrite /BZabs /BZm_of_nat; Ytac0; aw. have kz: inc (J k C1) BZp by apply: indexed_pi => //;apply:NS_diff. have le2: P (J k C1) <=c P (BZopp m) by rewrite BZopp_val; aw. move: (BZps_sBZp (BZopp_negative1 mn)) => omp. move / (zle_P1 kz omp): le2 => le3; BZo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)