proposition: Lemma rotate_characterization: forall n k, (k = 0 -> rotate n k = n) /\ (k > 0 -> k <= n -> rotate n k = k - 1) /\ (k > n -> rotate n k = k).
proof: Proof. intros; repeat split; intros; unfold rotate; just_do_it. Qed.
imports: Dblib.DblibTactics