proposition: Fact le0_add x y : 0 <= x -> 0 <= y -> 0 <= x + y.
proof: Proof. rewrite !le_def => /predU1P [<-|x_gt0]; first by rewrite add0r. by case/predU1P=> [<-|y_gt0]; rewrite ?addr0 ?x_gt0 ?lt0_add // orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(ssrAC div fintype path bigop order finset fingroup) mathcomp(ssralg poly)