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