proposition: Lemma Uinv_Nmult : forall k n, [1-] (k */ [1/]1+n) == ((S n) - k) */ [1/]1+n.
proof: Proof. intros k n; case (le_lt_dec (S n) k); intro. rewrite (Nmult_ge_Sn_Unth l). replace (S n - k)%nat with O; auto. lia. induction k; intros. rewrite Nmult_0; rewrite Uinv_zero. replace (S n - O)%nat with (S n); auto with arith. rewrite (Nmult_S k ([1/]1+n)). apply Uplus_eq_simpl_right with ([1/]1+n); auto. apply Uinv_le_perm_right. apply Nmult_le_n_Unth. lia. apply Oeq_trans with (((S n - S k) + (S O)) */ [1/]1+n). replace ((S n - S k) + (S O))%nat with (S n - k)%nat. apply Oeq_trans with ([1-] (k */ [1/]1+n)); auto with arith. apply Uinv_plus_left. apply Nmult_le_n_Unth; lia. lia. rewrite (plus_Nmult_distr (S n - S k) (S O) ([1/]1+n)); auto. Qed.
imports: ALEA(Utheory)