proposition: Lemma add1Pz (n : int) : 1 + (n - 1) = n.
proof: Proof. by case: (intP n)=> // n' /= _; rewrite ?(subn1, addn0). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)