How to model and prove hybrid systems with KeYmaera: a tutorial on safety