proposition: Lemma UnMoinsPos: (0 < Unmoins)%R.
proof: Proof. unfold Unmoins. assert (powerRZ radix (Z.succ (-p)) / 2 < 1)%R; auto with real. apply Rmult_lt_reg_l with 2%R; auto with real. apply Rle_lt_trans with (powerRZ radix (Z.succ (-p))); [right; field; auto with real| ring_simplify (2*1)%R]. apply Rle_lt_trans with (powerRZ radix (Z.succ (-1))); unfold Z.pred; auto with real zarith. apply Rle_powerRZ;try apply IZR_le; auto with zarith. simpl; auto with real. apply Rplus_lt_reg_l with (powerRZ radix (Z.succ (- p)) / 2)%R. ring_simplify; assumption. Qed.
imports: Reals ZArith List PeanoNat Psatz