proposition: Lemma x2y2Le: (Rabs (x2*y2) <= (powerRZ radix (2*s+Fexp x+Fexp y)) /4)%R.
proof: Proof. rewrite Rabs_mult. apply Rle_trans with ((powerRZ radix (s + Fexp x) / 2)*(powerRZ radix (s + Fexp y) / 2))%R. apply Rmult_le_compat; try apply Rabs_pos; auto with real. replace (2*s)%Z with (s+s)%Z; auto with zarith. repeat rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. right; field. Qed.
imports: Reals ZArith List PeanoNat Psatz