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