proposition: Lemma Ole_eq_compat : forall (O : ord) (x1 x2 : O), x1 == x2 -> forall x3 x4 : O, x3 == x4 -> x1 <= x3 -> x2 <= x4.
proof: Proof. firstorder; apply Ole_trans with x1; trivial. apply Ole_trans with x3; trivial. Qed.