Starting to learn coq

FWIW: just learned (on zulip) this was part of a challenge. That explains why somebody would make the problem so mean :-). My criticism of the teacher doesn’t apply.