The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Hi,

 Perhaps you've forgot to assume propositional extensionnality
(defined in Classicalfacts)

Your lemma can be rephrased into :

Require Import ClassicalFacts.
Fact orderbleb : prop_extensionality -> (fun a b : Unit =>
     is_true (orderb a b)) = order.

Pierre



Le 30/03/2016 13:12, Benoît Viguier a écrit :
> Require Import FunctionalExtensionality.
> Require Import Bool.
> Require Import Arith.
>
> Definition Unit := nat.
> Definition orderb := Nat.leb.
> Definition order := le.
>
> Fact orderbleb : (fun a b : Unit =>
>       is_true (orderb a b)) = order.
> Proof.
> apply functional_extensionality.
> intro a.
> apply functional_extensionality.
> intro b.
> unfold orderb.
> unfold is_true.
> unfold order.
> Check Nat.leb_le.
> rewrite Nat.leb_le.