proposition: Lemma rotate_nat_sub_0 base len : base < len → rotate_nat_sub base base len = 0.
proof: Proof. intros ?. rewrite rotate_nat_sub_alt by done. case_decide; lia. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)