proposition: Lemma Feq_mult : Feq I F F' -> Feq I G G' -> Feq I (F{*}G) (F'{*}G').
proof: Proof. intros H0 H1. elim H0; intros incF H0'. elim H0'; clear H0 H0'; intros incG H2. elim H1; intros incF' H1'. elim H1'; clear H1 H1'; intros incG' H0. FEQ; simpl in |- *; algebra. Qed.
imports: CoRN.reals.Intervals CoRN.tactics.DiffTactics1