proposition: Lemma Integral_strext' : forall c d Hcd HF1 HF2, Integral (Hab:=Hab) (F:=F) HF1 [#] Integral (a:=c) (b:=d) (Hab:=Hcd) (F:=F) HF2 -> a [#] c or b [#] d.
proof: Proof. intros c d Hcd HF1 HF2 H. elim (cg_minus_strext _ _ _ _ _ H); clear H; intro H; elim (integral_strext' _ _ _ _ _ _ _ _ _ H); clear H; intro H. elim (Min_strext_unfolded _ _ _ _ H); auto. auto. elim (Min_strext_unfolded _ _ _ _ H); auto. auto. Qed.
imports: CoRN.ftc.Integral CoRN.ftc.MoreFunctions