proposition: Lemma rotate_nat_sub_alt base offset len: base < len → offset < len → rotate_nat_sub base offset len = if decide (offset < base) then len + offset - base else offset - base.
proof: Proof. unfold rotate_nat_sub. intros ??. case_decide. - rewrite Z.mod_small by lia. by rewrite <-Nat2Z.inj_add, <-Nat2Z.inj_sub, Nat2Z.id 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)