proposition: Lemma rotate_nat_add_0 base len : base < len → rotate_nat_add base 0 len = base.
proof: Proof. intros ?. unfold rotate_nat_add. rewrite Z.mod_small by lia. by rewrite Z.add_0_r, Nat2Z.id. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)