The Coq mailing list

["Strub, Pierre-Yves" <pierre-yves AT strub.nu>]

Hi,

You can search for addIr in ssralg.v to see such a proof.

Best,
-- Pierre-Yves.

On 2014-08-13 02: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