proposition: Lemma integral_empty : a [=] b -> Integral F contF [=] [0].
proof: Proof. intros. unfold integral in |- *. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply Lim_const. apply Lim_wd'. intros; simpl in |- *. unfold integral_seq, Even_Partition_Sum, Partition_Sum in |- *. apply eq_transitive_unfolded with (Sumx (fun (i : nat) (H : i < S n) => ZeroR)). apply Sumx_wd; intros; simpl in |- *. eapply eq_transitive_unfolded. apply dist_2a. apply x_minus_x. apply mult_wdr. apply bin_op_wd_unfolded. algebra. astepl (nring (S i) [*] (b[-]b[/] _[//]nring_ap_zero' _ _ (O_S n))). astepr (nring i[*] (b[-]b[/] _[//]nring_ap_zero' _ _ (O_S n))). rational. eapply eq_transitive_unfolded. apply sumx_const. algebra. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)