proposition: Lemma oppzD : {morph oppz : m n / m + n}.
proof: Proof. by move=> [[|n]|n] [[|m]|m] /=; rewrite ?addn0 ?subn0 ?addnS //; rewrite !NegzE !ltnS !subSS; case: ltngtP => [?|?|->]; rewrite ?subnn // ?oppzK ?subnS ?prednK // subn_gt0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)