proposition: Lemma half_esp_le : forall x, x <= ([1/2]) * (x & x) + [1/2].
proof: Proof. intros; apply (Ule_total ([1/2]) x); intros; auto. setoid_rewrite (half_esp _ H); trivial. assert (x & x == 0); auto. setoid_rewrite H0. setoid_rewrite (Umult_zero_right ([1/2])). setoid_rewrite (Uplus_zero_left ([1/2])); auto. Qed.
imports: ALEA(Utheory)