proposition: Lemma bnd_away_zero_square : bnd_away_zero I (F{*}F).
proof: Proof. elim Fbnd; clear Fbnd; intros H H0. elim H0; clear H0; intros x H1 H2. split. Included. exists (x[*]x). astepl (ZeroR[*][0]); apply mult_resp_less_both; try apply leEq_reflexive; assumption. intros y Hy H0. unfold I in H; apply leEq_wdr with (AbsIR (FRestr H y H0)[*]AbsIR (FRestr H y H0)). apply mult_resp_leEq_both; try (apply less_leEq; assumption); simpl in |- *; apply H2; try assumption. eapply eq_transitive_unfolded. apply eq_symmetric_unfolded; apply AbsIR_resp_mult. apply AbsIR_wd; simpl in |- *; rational. Qed.
imports: CoRN.ftc.Derivative