This probably isn't a simple nor use-friendly intro, but it's pretty comprehensive at least: https://flint.cs.yale.edu/cs430/coq/pdf/Tutorial.pdf (section 1.2 has the first minimal proof, although familiarity with formal logic is kind of a pre-req to properly parsing this style of writing)

I remember learning and using Coq in a similar 300-level CS course at my university, 10+ years ago.