Ssreflect Users Discussion List

[<>]

Hello.

I have a question about subgoal generating rewrite tactics.
Is there a better way of do a similar thing to below?

  Require Import ssreflect.
   
  Variable f: nat -> nat.
  
  Axiom  f_flat: forall a, a = 0 -> f a = 0.
  
  Goal forall a, a*a = 0 -> f a + 1 = 1 .
  move => a ha.
  rewrite (_ : f_flat a _).

The last line does not work.
What I want is to rewrite the goal to "0 + 1 = 1" 
and generate subgoal "a = 0", 
although I somehow feel I am messing up something.

By the way, the link to this mailing list from 
http://www.msr-inria.inria.fr/Projects/math-components
seems broken; it refers to http instead of https.


With best regards,
Keiko