proposition: Lemma Nmult_Unth_le : 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 Ole_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_le_compat_right. rewrite (Nmult_Unth_simpl_right n1 ([1/]1+m1)); auto. apply Ole_trans with ((m2 * S m1) */ [1/]1+m1 * [1/]1+n1); auto. rewrite (Nmult_mult_assoc m2 (S m1) ([1/]1+m1 * [1/]1+n1)). apply Nmult_le_compat_right. rewrite (Nmult_Unth_simpl_left m1 ([1/]1+n1)); auto. Qed.
imports: ALEA(Utheory)