proposition: Lemma compact_inc_Min_rht : forall H, included (compact (Min a b) b H) (Compact Hab).
proof: Proof. intros. apply included_compact; split. apply leEq_reflexive. apply Min_leEq_Max. apply Min_leEq_rht. apply rht_leEq_Max. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions