proposition: Lemma rotate_nat_sub_lt base offset len : 0 < len → rotate_nat_sub base offset len < len.
proof: Proof. unfold rotate_nat_sub. intros ?. pose proof (Z_mod_lt (Z.of_nat len + Z.of_nat offset - Z.of_nat base) (Z.of_nat len)). apply Nat2Z.inj_lt. rewrite Z2Nat.id; lia. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)