proposition: Lemma Feq_recip : bnd_away_zero I F -> Feq I F F' -> Feq I {1/}F {1/}F'.
proof: Proof. intros Hbnd H0. elim H0; intros incF H0'. elim H0'; clear H0 H0'; intros incF' H1. FEQ. apply included_FRecip. auto. intros x H Hx; apply ap_wdl_unfolded with (F x (incF x H)). apply bnd_imp_ap_zero with I; assumption. auto. simpl in |- *; algebra. Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1