proposition: Lemma Feq_recip' : bnd_away_zero I F -> Feq I F' F -> Feq I {1/}F' {1/}F.
proof: Proof. intros. apply Feq_symmetric; apply Feq_recip. assumption. apply Feq_symmetric; assumption. Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1