proposition: Lemma addSnz (m : nat) (n : int) : (m.+1%N) + n = 1 + (m + n).
proof: Proof. move: m n=> [|m] [] [|n] //=; rewrite ?add1n ?subn1 // !(ltnS, subSS). case: ltngtP=> hnm /=; rewrite ?hnm ?subnn //. by rewrite subnS add1n prednK ?subn_gt0. by rewrite ltnS leqn0 subn_eq0 leqNgt hnm /= subnS subn1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(fintype finfun bigop order ssralg countalg ssrnum) mathcomp(poly)