proposition: Lemma Udiv_plus : forall x y z, (x+y)/z == x/z + y/z.
proof: Proof. intros; apply Ole_antisym; auto. apply (Ueq_orc 0 z); auto; intros. repeat (rewrite Udiv_by_zero; auto). apply (Ule_total x z); auto; intros. apply (Ule_total y z); auto; intros. apply (Ule_total (x/z) ([1-](y/z))); auto; intros. apply Umult_div_le_right; auto. rewrite Udistr_plus_right; auto. apply Uplus_le_compat; rewrite Udiv_mult; auto. rewrite (Uplus_one (x/z) (y/z)); auto. rewrite (Udiv_le_one y H); auto. apply Ole_trans with 1; auto. rewrite (Udiv_le_one x H); auto. apply Ole_trans with 1; auto. Qed.
imports: ALEA(Utheory)