coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Frederic Blanqui <frederic.blanqui AT inria.fr>
- To: Jean-Francois Monin <Jean-Francois.Monin AT imag.fr>
- Cc: roconnor AT theorem.ca, Coq Club <coq-club AT pauillac.inria.fr>, sebastien.hinderer AT loria.fr
- Subject: Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2.
- Date: Sat, 25 Oct 2008 12:20:53 +0800
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Jean-Francois Monin a écrit :
Lemma LE_le : forall n m, LE n m -> n <= m.
Lemma le_LE : forall n m, n <= m -> LE n m.
Just a small additional remark: I suggest to use <-> here so that you can use the rewrite tactic!
- Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2., Jean-Francois Monin
- Re: [Coq-Club] forall n m (H1 H2:le n m), H1=H2., Frederic Blanqui
Archive powered by MhonArc 2.6.16.