proposition: Lemma fmon_le_compat2 : forall (O1 O2 O3:ord) (f: O1 -m> O2 -m> O3) (x y:O1) (z t:O2), x<=y -> z <=t -> f x z <= f y t.
proof: Proof. intros; apply Ole_trans with (f x t). apply (fmonotonic (f x)); auto. apply (fmonotonic f); auto. Qed.