proposition: Lemma fplusok_le_compat : forall (A:Type)(f1 f2 g1 g2:MF A), fplusok f2 g2 -> f1 <= f2 -> g1 <= g2 -> fplusok f1 g1.
proof: Proof. unfold fplusok; intros. apply Ole_trans with f2; trivial. apply Ole_trans with (finv g2); trivial. apply finv_le_compat; auto. Qed.
imports: ALEA(Uprop) ALEA(Utheory)