proposition: Lemma truncD : {in nat_num & Rnneg, {morph trunc : x y / x + y >-> (x + y)%N}}.
proof: Proof. move=> _ y /natrP[n ->] y_ge0; apply: trunc_def. by rewrite -addnS !natrD !natrK lerD2l ltrD2l trunc_itv. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order ssralg poly ssrnum ssrint)