proposition: Lemma integral_wd' : forall a' b' Hab' contF', a [=] a' -> b [=] b' -> Integral F contF [=] integral a' b' Hab' F contF'.
proof: Proof. intros. unfold integral in |- *. apply Lim_wd'. intro; simpl in |- *. unfold integral_seq, Even_Partition_Sum, Partition_Sum in |- *. apply Sumx_wd; intros; apply mult_wd. apply pfwdef; simpl in |- *; algebra. simpl in |- *. repeat first [ apply cg_minus_wd | apply bin_op_wd_unfolded | apply mult_wd | apply div_wd ]; algebra. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)