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