proposition: Lemma half_le : forall x y, y <= [1-] y -> x <= y + y -> ([1/2]) * x <= y.
proof: Proof. intros. apply not_Ult_le; red; intros. assert (y + y < x); auto. apply Ult_le_trans with (mean x x); auto. unfold mean; apply Uplus_lt_compat; auto. Qed.
imports: ALEA(Utheory)