proposition: Lemma Nmult_Unth_simpl_left : forall n x, (S n) */ ([1/]1+n * x) == x.
proof: Proof. intros. rewrite (Nmult_Umult_assoc_left (S n) ([1/]1+n) x (Nmult_def_Unth n)). rewrite (Nmult_Sn_Unth n); auto. Qed.
imports: ALEA(Utheory)