proposition: Lemma Udiv_inv : forall x y, ~0==y -> [1-](x/y) <= ([1-]x)/y.
proof: Proof. intros; apply (Ule_total x y); auto; intros. apply Umult_div_le_left; auto. apply Ole_trans with ([1-] (x/y * y)); auto. rewrite Udiv_le_one; auto. Qed.
imports: ALEA(Utheory)