proposition: Lemma discrete_stable_inv : forall A (c : nat -> U) (p : nat -> A), wretract c -> stable_inv (discrete c p).
proof: Proof. red; intros. repeat rewrite discrete_simpl. unfold finv; apply serie_inv_le; auto. Qed.
imports: ALEA(Monads) ALEA(Utheory)