proposition: Lemma zshiftP z m : shift m z = z + m.
proof: Proof. elim: m => [| m ihm]; first by rewrite addr0. by rewrite shiftE /= -shiftE ihm -addn1 PoszD addrA. Qed.
imports: BinInt ZifyClasses mathcomp(all_ssreflect all_algebra) tactics