Fix indications about rewrite tactic in vanilla Rocq vs. ssreflect - #1

Open

matematiflo wants to merge 1 commit into

Tragicus:mainfrom

matematiflo:main

Commits on Apr 20, 2026

Fix indications about rewrite tactic in vanilla Rocq vs. ssreflect, add corresponding solution to the vanilla Rocq version
matematiflo
committed
6631700