proposition: Lemma Udiv_minus : forall x y z, ~0 == z -> x <= z -> (x - y) / z == x/z - y/z.
proof: Proof. intros; apply (Ule_total x y); auto; intros. apply Oeq_trans with (0/z); auto. rewrite Uminus_le_zero; auto. assert (y <= z). apply Ole_trans with x; auto. apply Oeq_sym; apply Umult_div_eq; auto. rewrite Uminus_distr_left. rewrite Udiv_mult; auto. rewrite Udiv_mult; auto. Qed.
imports: ALEA(Utheory)