proposition: Lemma Udiv_eq_compat_right : forall x y z, y == z -> x/z == x/y.
proof: Proof. intros; apply (Ueq_orc 0 y); auto; intros. assert (0==z). rewrite <- H; auto. repeat rewrite Udiv_by_zero; auto. assert ( ~ 0 == z). apply Ule_neq_zero with y; auto. apply Ole_antisym; auto. Qed.
imports: ALEA(Utheory)