The Coq mailing list

[Jonas Oberhauser <s9joober AT gmail.com>]

Am 25.11.2012 13:53, schrieb Gert Smolka:
> Lemma gcd_ref x y :
>    x=y -> gcd (x,y) = x.

Have you tried this:

Definition pi1 {X Y} (p : X * Y) := let (x,_) := p in x.
Definition pi2 {X Y} (p : X * Y) := let (_,y) := p in y.

Lemma gcd_ref p :
  pi1 p = pi2 p -> gcd p = pi1 p.

Kind regards, jonas