proposition: Lemma integral_strext' : forall c d Hcd HF1 HF2, integral a b Hab F HF1 [#] integral c d Hcd F HF2 -> a [#] c or b [#] d.
proof: Proof. intros c d Hcd HF1 HF2 H. clear contF contG. unfold integral in H. elim (Lim_strext _ _ H). clear H; intros N HN. simpl in HN. unfold integral_seq, Even_Partition_Sum, Partition_Sum in HN. set (f1 := fun (i : nat) (Hi : i < S N) => Part _ _ (contin_imp_inc _ _ _ _ HF1 _ (Pts_part_lemma _ _ _ _ _ _ (Partition_imp_points_1 _ _ _ _ (Even_Partition Hab _ (O_S N))) i Hi)) [*] (Even_Partition Hab _ (O_S N) _ Hi[-] Even_Partition Hab _ (O_S N) _ (Nat.lt_le_incl _ _ Hi))) in *. set (f2 := fun (i : nat) (Hi : i < S N) => Part _ _ (contin_imp_inc _ _ _ _ HF2 _ (Pts_part_lemma _ _ _ _ _ _ (Partition_imp_points_1 _ _ _ _ (Even_Partition Hcd _ (O_S N))) i Hi)) [*] (Even_Partition Hcd _ (O_S N) _ Hi[-] Even_Partition Hcd _ (O_S N) _ (Nat.lt_le_incl _ _ Hi))) in *. cut (nat_less_n_fun f1); intros. cut (nat_less_n_fun f2); intros. elim (Sumx_strext _ _ _ _ H H0 HN). clear H0 H HN; intros i Hi. elim Hi; clear Hi; intros Hi Hi'. unfold f1, f2 in Hi'; clear f1 f2. elim (bin_op_strext_unfolded _ _ _ _ _ _ Hi'); clear Hi'; intro. assert (H := pfstrx _ _ _ _ _ _ a0). clear a0; simpl in H. elim (bin_op_strext_unfolded _ _ _ _ _ _ H); clear H; intro. left; auto. elim (bin_op_strext_unfolded _ _ _ _ _ _ b0); clear b0; intro. exfalso; generalize a0; apply ap_irreflexive_unfolded. elim (div_strext _ _ _ _ _ _ _ b0); clear b0; intro. elim (cg_minus_strext _ _ _ _ _ a0); clear a0; intro. right; auto. left; auto. exfalso; generalize b0; apply ap_irreflexive_unfolded. elim (cg_minus_strext _ _ _ _ _ b0); clear b0; intro. simpl in a0. elim (bin_op_strext_unfolded _ _ _ _ _ _ a0); clear a0; intro. left; auto. elim (bin_op_strext_unfolded _ _ _ _ _ _ b0); clear b0; intro. exfalso; generalize a0; apply ap_irreflexive_unfolded. elim (div_strext _ _ _ _ _ _ _ b0); clear b0; intro. elim (cg_minus_strext _ _ _ _ _ a0); clear a0; intro. right; auto. left; auto. exfalso; generalize b0; apply ap_irreflexive_unfolded. elim (bin_op_strext_unfolded _ _ _ _ _ _ b0); clear b0; intro. left; auto. elim (bin_op_strext_unfolded _ _ _ _ _ _ b0); clear b0; intro. exfalso; generalize a0; apply ap_irreflexive_unfolded. elim (div_strext _ _ _ _ _ _ _ b0); clear b0; intro. elim (cg_minus_strext _ _ _ _ _ a0); clear a0; intro. right; auto. left; auto. elim (bin_op_strext_unfolded _ _ _ _ _ _ b0); clear b0; intro. exfalso; generalize a0; apply ap_irreflexive_unfolded. exfalso; generalize b0; apply ap_irreflexive_unfolded. red in |- *. do 3 intro. rewrite H0; clear H0; intros. unfold f2 in |- *. algebra. red in |- *. do 3 intro. rewrite H; clear H; intros. unfold f1 in |- *. algebra. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)