proposition: Lemma nds_small_nz_shift x: nds_small_nz x -> nds_small_nz (nds_shift x).
proof: Proof. move => [ha hb]; split; first by apply: (oprod2_pos (oopow_pos OS2) ha). move: (oprod_Meqlt hb (oopow_pos OS2)). by rewrite - (opow_sum OS_omega OS2 OS_omega) (osum_int_omega olt_2omega). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)