proposition: Lemma qle_triangular n m: ratp n -> ratp m -> (BQabs (n +q m)) <=q (BQabs n) +q (BQabs m).
proof: Proof. move: n m. pose aux n m := BQabs (n +q m) <=q BQabs n +q BQabs m. suff: forall n m, inc n BQp -> ratp m -> aux n m. move => h n m; case /BQ_i0P; last by apply: h. move => pa pb; rewrite - (BQabs_opp) - (BQabs_opp n)- (BQabs_opp m). rewrite (BQoppD (BQms_sBQ pa) pb); apply: h (QSo pb). apply:(BQopp_negative2 (BQms_sBQm pa)). move => n m np; case /BQ_i0P; last first. move => mp; rewrite /aux (BQabs_pos np) (BQabs_pos mp). move:(QpS_sum np mp) => pa; move: (BQp_sBQ pa) => pb. rewrite (BQabs_pos pa); apply: (qleR pb). move => mn; rewrite /aux. move: (BQp_sBQ np) (BQms_sBQ mn) => nq mq. have pa : \0q <=q BQabs n +q BQabs m. by apply / qle0xP; apply: (QpS_sum);apply: QpSa. case /BQ_i1P: (QSs nq mq) => sa. + by rewrite sa BQabs_0. + rewrite (BQabs_pos (BQps_sBQp sa)). move: (qle_abs mq); rewrite (BQabs_pos np). by move /(BQsum_le2l mq (QSa mq) nq). + rewrite (BQabs_negs sa) (BQabs_pos np) (BQabs_negs mn). rewrite (BQoppD nq mq). apply/(@BQsum_le2r (BQopp n) n (BQopp m) (QSo nq) nq (QSo mq)). move / qge0xP: (BQopp_positive2 np) => sb. move/ qle0xP: np => sc; BQo_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)