proposition: Lemma addzA : associative addz.
proof: Proof. elim=> [|m ihm|m ihm] n p; first by rewrite !add0z. by rewrite -add1n PoszD !addSz ihm. by rewrite -add1n addnC PoszD oppzD !addPz ihm. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)