proposition: Lemma Nmult_Unth_eq : forall (n1 n2 m1 m2:nat), (n2 * S n1= m2 * S m1)%nat -> n2 */ [1/]1+m1 == m2 */ [1/]1+n1.
proof: Proof. intros. apply Oeq_trans with ((n2 * S n1) */ ([1/]1+m1 * [1/]1+n1)). rewrite (Nmult_mult_assoc n2 (S n1) ([1/]1+m1 * [1/]1+n1)). apply Nmult_eq_compat_left; auto. rewrite H. rewrite (Nmult_mult_assoc m2 (S m1) ([1/]1+m1 * [1/]1+n1)). apply Nmult_eq_compat_left; auto. Qed.
imports: ALEA(Utheory)