proposition: Lemma Unth_not_null : forall n, ~ (0 == [1/]1+n).
proof: Proof. red; intros. apply Udiff_0_1. apply Oeq_trans with ([1/]1+n); auto. apply Oeq_trans with ([1-] (sigma (fun k => [1/]1+n) n)). apply (Unth_prop n). apply Oeq_trans with ([1-] (sigma (fun k => 0) n)). apply Uinv_eq_compat. apply sigma_eq_compat; auto. apply Oeq_trans with ([1-] 0); auto. Qed.
imports: ALEA(Utheory)