Utilities for course statements

Sometimes a course states a result much earlier than it proves it, or states a theorem that won't be proved in the course.

axiom proved_later {P : Prop} : P

This theorem is proved later in this course.

axiom blackboxed {P : Prop} : P

This theorem is not proved in this course but will be used.

axiom showcased {P : Prop} : P

This theorem is not proved in this course and won't be used.