proposition: Lemma rle_triangular x y: realp x -> realp y -> (BRabs (x +r y)) <=r (BRabs x) +r (BRabs y).
proof: Proof. move: x y. pose aux n m := BRabs (n +r m) <=r BRabs n +r BRabs m. suff: forall n m, inc n BRp -> inc m BR -> aux n m. move => h n m; case /BR_i0P; last by apply: h. move => pa pb; move: (BRms_sBR pa) => pc. rewrite - (BRabs_opp (RSs pc pb)) - (BRabs_opp pb) -(BRabs_opp pc). rewrite (BRoppD pc pb); apply: h (RSo pb). apply:BRopp_negative2 (BRms_sBRm pa). move => n m np; case /BR_i0P; last first. move => mp; rewrite /aux (BRabs_pos np) (BRabs_pos mp). move:(RpS_sum np mp) => pa; move: (BRp_sBR pa) => pb. rewrite (BRabs_pos pa); apply: (rleR pb). move => mn; rewrite /aux. move: (BRp_sBR np) (BRms_sBR mn) => nq mq. have pa : \0r <=r BRabs n +r BRabs m. by apply / rle0xP; apply: (RpS_sum);apply: RpSa. case /BR_i1P: (RSs nq mq) => sa. + by rewrite sa BRabs_0. + rewrite (BRabs_poss sa). move: (rle_abs mq); rewrite (BRabs_pos np). by move /(BRsum_le2l mq (RSa mq) nq). + rewrite (BRabs_negs sa) (BRabs_pos np) (BRabs_negs mn). rewrite (BRoppD nq mq). apply/(BRsum_le2r (RSo nq) nq (RSo mq)). move / rge0xP: (BRopp_positive2 np) => sb. move/ rle0xP: np => sc; BRo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)