proposition: Lemma positive_norm : [0] [<=] Norm_Funct.
proof: Proof. apply leEq_transitive with (AbsIR (FRestr Hinc' a (compact_inc_lft _ _ _))). apply AbsIR_nonneg. simpl in |- *; apply norm_bnd_AbsIR; unfold I in |- *; apply compact_inc_lft. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac