proposition: Lemma FNorm_wd : Feq I F G -> FNorm I cI F contF [=] FNorm I cI G contG.
proof: Proof. intro H; unfold FNorm in |- *; apply Norm_Funct_wd. eapply included_Feq. 2: apply H. Included. Qed.
imports: CoRN.ftc.MoreIntervals