proposition: Theorem square : forall x : R, forall xi zi : FF, ABS x xi -> square_helper xi zi = true -> BND (x * x) zi.
proof: Proof. intros x xi zi (Hx1,Hx2) Hb. generalize (andb_prop _ _ Hb). clear Hb. intros (H1,H2). fold (Rsqr x). rewrite Rsqr_abs. apply mul_pp with (1 := Hx2) (2 := Hx2). unfold mul_pp_helper. rewrite H1, H2. apply Float_prop.ge_0_F2R in Hx1. revert Hx1. unfold Fpos0. now case (Fnum (lower xi)). Qed.
imports: Gappa_common Gappa_decimal