The Coq mailing list

["Terrell, Jeffrey" <jeffrey.terrell AT kcl.ac.uk>]

Require Import Plus.

Fact Cancellation_Law: forall x y z, x + z = y + z -> x = y.
Proof.
   intros.
   apply (plus_reg_l x y z).
   rewrite (plus_comm x z) in H.
   rewrite (plus_comm y z) in H.
   assumption.
Qed.

Regards,
Jeff.

On 13 Aug 2014, at 01:42, Jinfang Wang wrote:

> 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