proposition: Lemma le_minus_distr : forall (A : Type)(m:M A), forall (f g:A -> U), m (fminus f g) <= m f.
proof: Proof. intros A m; intros. apply (fmonotonic m); intro x; rewrite fminus_eq; auto. Qed.
imports: ALEA(Uprop) ALEA(Utheory)