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