proposition: Lemma half_esp : forall x, ([1/2] <= x) -> ([1/2]) * (x & x) + [1/2] == x.
proof: Proof. intros; unfold Uesp. setoid_rewrite (Uinv_half ([1-] x + [1-] x)). assert (H1:[1-] x <= [1/2]). setoid_rewrite Unth_one; auto. rewrite (half_twice _ H1); auto. Qed.
imports: ALEA(Utheory)