proposition: Lemma addr_ge0 x y : 0 <= x -> 0 <= y -> 0 <= x + y.
proof: Proof. rewrite le0r; case/predU1P=> [-> | x_pos]; rewrite ?add0r // le0r. by case/predU1P=> [-> | y_pos]; rewrite ltW ?addr0 ?addr_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)