proposition: Lemma Umult_le_simpl_right : forall x y z, ~0 == z -> (x * z) <= (y * z) -> x <= y.
proof: Proof. intros; apply Umult_le_simpl_left with z; auto. setoid_rewrite (Umult_sym z x); setoid_rewrite (Umult_sym z y);trivial. Qed.
imports: ALEA(Utheory)