proposition: Lemma half_twice_le : forall x, ([1/2]) * (x + x) <= x.
proof: Proof. intros; apply (Ule_total x ([1/2])); intros; auto. rewrite (half_twice _ H); trivial. assert (x+x==1); auto. rewrite H0. rewrite (Umult_one_right ([1/2])); auto. Qed.
imports: ALEA(Utheory)