proposition: Lemma Nmult_le_simpl : forall (n:nat) (x y:U), Nmult_def (S n) x -> Nmult_def (S n) y -> (S n */ x) <= (S n */ y) -> x <= y.
proof: Proof. intros; apply Umult_le_simpl_left with (S n */ [1/]1+n). auto. assert (Nmult_def (S n) ([1/]1+n)); auto. rewrite <- (Nmult_Umult_assoc_left (S n) ([1/]1+n) x H2). rewrite <- (Nmult_Umult_assoc_left (S n) ([1/]1+n) y H2). rewrite (Nmult_Umult_assoc_right (S n) ([1/]1+n) y H0). rewrite (Nmult_Umult_assoc_right (S n) ([1/]1+n) x H). apply Ole_trans with ([1/]1+n * (S n */ x)); auto. Qed.
imports: ALEA(Utheory)