proposition: Lemma Nmult_Umult_assoc_left : forall n x y, Nmult_def n x -> n*/(x*y) == (n*/x)*y.
proof: Proof. intros n x y; induction n; auto; intros. destruct n; auto. repeat rewrite Nmult_SS. assert(Nmult_def (S n) x); auto. setoid_rewrite (IHn H0). assert (x <= [1-] ((S n) */ x)). apply Uinv_le_perm_right. apply Ole_trans with ([1-] ([1/]1+(S n))); auto. apply Ole_trans with ((S n) */ ([1/]1+(S n))); auto. apply Oeq_sym; auto. Qed.
imports: ALEA(Utheory)