The Coq mailing list

[Jinfang Wang <wang AT math.s.chiba-u.ac.jp>]

Dear All,

I am a statistician and am (very) new to Coq/SSReflect.

I am asking a shamefully simple question, namely, what kind of tactics should I use to cancel a common factor from both sides of an equation? In its simplest form, I what to know how to prove the following fact:

Fact Cancellation_Law: forall x y z, x + z = y + z -> x=y.

Thanks a lot for your help.

Jinfang Wang

Chiba University, Japan