proposition: Lemma Integral_empty : a [=] b -> Integral contF [=] [0].
proof: Proof. intros. unfold Integral in |- *. astepr (ZeroR[-][0]). apply cg_minus_wd; apply integral_empty. astepr a; apply leEq_imp_Min_is_lft; apply eq_imp_leEq; assumption. apply leEq_imp_Min_is_lft; apply eq_imp_leEq; assumption. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions