The Coq mailing list

[Florian Hatat <florian.hatat AT ens-lyon.fr>]

Hi,

Wan Hai a écrit :
> forall m1 m2 n, fc n (fun x=>m1*m2*x) = fc n (fun x=>m2*m1*x)
> (...)
> Is there another way to prove this not using the extensionality axiom
In this particular case (since you can rewrite using the equality
m1*m2*x = m2*m1*x, see the mult_comm lemma in Mult), you do not need the
extensionality axiom.

Theorem th1 : forall m1 m2 n, fc n (fun x=>m1*m2*x) = fc n (fun x=>m2*m1*x).
Proof.
intros m1 m2 n.
rewrite (mult_comm m1 m2).
reflexivity.
Qed.

By the way, I would be curious to known whether there exists an
unprovable (without extensionality) equality between two nat's...

-- 
Florian,
http://openweb.eu.org/
http://www.linux-france.org/

Attachment: signature.asc
Description: OpenPGP digital signature