proposition: Lemma Unth_half : forall n, (O<n)%nat -> [1/]1+(pred (n+n)) == [1/2] * [1/]1+pred n.
proof: Proof. intros; apply Oeq_sym; apply Unth_eq. destruct n; intros. absurd (0<0)%nat; auto with arith. simpl. replace (n + S n)%nat with (2 * n + 1)%nat; auto with zarith. rewrite plus_Nmult_distr. rewrite Nmult_1. rewrite Nmult_mult_assoc. rewrite Nmult_Umult_assoc_right; auto. rewrite Nmult_Umult_assoc_left; auto. rewrite Nmult_Sn_Unth. rewrite Umult_one_left. rewrite Nmult_n_Unth. rewrite Udistr_inv_right; auto. Qed.
imports: ALEA(Utheory)