proposition: Lemma rotate_nat_sub_add base len offset: offset < len → rotate_nat_sub base (rotate_nat_add base offset len) len = offset.
proof: Proof. intros ?. unfold rotate_nat_add, rotate_nat_sub. rewrite Z2Nat.id by (apply Z.mod_pos; lia). assert (∀ n, (Z.of_nat len + n - Z.of_nat base) = ((Z.of_nat len - Z.of_nat base) + n))%Z as -> by naive_solver lia. rewrite Zplus_mod_idemp_r. replace (Z.of_nat len - Z.of_nat base + (Z.of_nat base + Z.of_nat offset))%Z with (Z.of_nat len + Z.of_nat offset)%Z by lia. rewrite (Z.mod_in_range 1) by lia. rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)