proposition: Lemma fmon_app_le_compat : forall (O1 O2 O3:ord) (f g:O1 -m> (O2 -m> O3)) (x y:O2), f <= g -> x <= y -> f <_> x <= g <_> y.
proof: Proof. red; intros; simpl; intros; auto. apply Ole_trans with (f x0 y); auto. apply (fmonotonic (f x0)); auto. Qed.