Generalise FunOrder

[agontard]

In the following:

analysis/classical/boolp.v

Lines 950 to 951 in 8d9538a

	HB.instance Definition _ := @Order.isPOrder.Build
	fun_display (aT -> T) lef ltf ltf_def lef_refl lef_anti lef_trans.

A->B is declared as a porderType when B is one. Wouldn't it be better to first declare A -> B as a preorderType when B is a preorderType?

[affeldt-aist]

Maybe. (MathComp's preorders arrived recently.)