I was going through the trivial example in this question How can I rewrite "+ 1" (plus one) to "S" (succ) in Coq? but the proof does not work in my local computer despite it workin...

I am expecting something in my messages bar but I don't see it Example script: Fixpoint add_left (n m : nat) : nat := match n with | O => m | S p => S (add_left p m) end. Lemma demo_1...