Buenas!
Me tranqué con este lema
forall n :nat, ~(O=n /\ (exists m :nat, n = (S m))).
No me doy cuenta como encararlo. Aplicando inicialmente un unfold not llego a un False, y de ahi aplico un absurdo.
No se si estoy aplicando mal el absurdo o hay que hacer un rewrite previamente.
Agradezco sugerencias!
Saludos!