It seems there is no way to saturate the key (forall _,_). Cf. https://github.com/damien-pous/partial-orders/blob/eb3b26da87156f8ecab28169e7b190365403c194/theories/lattice.v#L17 Merci @CohenCyril ;)
