The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 14/03/2017 00:28, Valentin Robert wrote:
> Hello,
> 
> Are there any existing techniques to either:
> 
> 1) allow rewriting with equations/inequations where the term to be
> rewritten is not immediately found, but can be isolated:
> 
> Require Import Reals.
> Example e1 (a b c d e : R) (H : c * a = d) : a * b * c = e.
> (* super_rewrite with H, to obtain something like (d * b = e) or (b * d
> = e) *)

If you don't need anything more clever than that, then "ring_simplify
[H]" does the job.

Best regards,

Guillaume