proposition: Lemma fmult_fplusok : forall (A:Type) p q (f1 f2 : A -> U), fplusok f1 f2 -> fplusok (fmult p f1) (fmult q f2).
proof: Proof. unfold fplusok, fmult, finv; intros; intro x. apply Ole_trans with (f1 x); auto. apply Ole_trans with ([1-]f2 x); auto. Qed.
imports: ALEA(Probas) ALEA(Utheory)