The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Coq Users,

 

the standard library file Coq.Structures.Orders.v contains the comment:

 

For stating properties like transitivity of leb, we coerce bool into Prop.

 

which makes me think there is a better way than tedious manual proofs for things like transitivity or irreflexivity of ltb, but I couldn’t find it. I added

 

Local Coercion is_true : bool >-> Sortclass.

 

but I don’t see how this would help me to e.g. get a trivial proof for

 

Lemma ltb_irrefl: forall x : t, ltb x x = false.

 

Thanks & best regards,

 

Michael