proposition: Lemma Continuous_I_min : Continuous_I Hab (FMin F G).
proof: Proof. unfold FMin in |- *. apply Continuous_I_inv; apply Continuous_I_max; apply Continuous_I_inv; auto. Qed.
imports: CoRN.reals.NRootIR CoRN.ftc.FunctSums CoRN.tactics.CornTac