proposition: Lemma integral_strext : Integral F contF [#] Integral G contG -> {x : IR | I x | forall Hx Hx', F x Hx [#] G x Hx'}.
proof: Proof. intro H. unfold integral in H. elim (Lim_ap_imp_seq_ap' _ _ H); intros N HN; clear H. simpl in HN. unfold integral_seq, Even_Partition_Sum, Partition_Sum in HN. set (f' := fun (i : nat) (H : i < S N) => Part F _ (contin_imp_inc _ _ _ _ contF _ (compact_partition_lemma _ _ Hab _ (O_S N) _ (Nat.lt_le_incl _ _ H))) [*] (Even_Partition Hab _ (O_S N) _ H[-] Even_Partition Hab _ (O_S N) i (Nat.lt_le_incl _ _ H))) in *. set (g' := fun (i : nat) (H : i < S N) => Part G _ (contin_imp_inc _ _ _ _ contG _ (compact_partition_lemma _ _ Hab _ (O_S N) _ (Nat.lt_le_incl _ _ H))) [*] (Even_Partition Hab _ (O_S N) _ H[-] Even_Partition Hab _ (O_S N) i (Nat.lt_le_incl _ _ H))) in *. cut (nat_less_n_fun f'); intros. cut (nat_less_n_fun g'); intros. cut (Sumx f' [#] Sumx g'). intros H1. elim (Sumx_strext _ _ _ _ H H0 H1). intros n Hn. elim Hn; clear Hn; intros Hn H'. exists (a[+]nring n[*] (b[-]a[/] nring _[//]nring_ap_zero' _ _ (O_S N))). unfold I in |- *; apply compact_partition_lemma; auto. apply Nat.lt_le_incl; assumption. intros. elim (bin_op_strext_unfolded _ _ _ _ _ _ H'); clear H'; intro. eapply ap_wdl_unfolded. eapply ap_wdr_unfolded. apply a0. algebra. algebra. exfalso; generalize b0; exact (ap_irreflexive_unfolded _ _). eapply ap_wdl_unfolded. eapply ap_wdr_unfolded. apply HN. unfold g', Partition_imp_points in |- *; apply Sumx_wd; intros; simpl in |- *; rational. unfold f', Partition_imp_points in |- *; apply Sumx_wd; intros; simpl in |- *; rational. do 3 intro. rewrite H0; unfold g' in |- *; intros; algebra. do 3 intro. rewrite H; unfold f' in |- *; intros; algebra. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)