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 Hbnd H0 H1. elim H0; intros incF H0'. elim H0'; clear H0 H0'; intros incF' H2. elim H1; intros incG H1'. elim H1'; clear H1 H1'; intros incG' H0. FEQ. apply included_FDiv; auto. intros x H Hx; apply ap_wdl_unfolded with (G x (incG x H)). apply bnd_imp_ap_zero with I; assumption. auto. simpl in |- *; algebra. Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1