proposition: Lemma integral_one : forall H, Integral ( [-C-] [1]) H [=] b[-]a.
proof: Proof. intro. unfold integral in |- *. eapply eq_transitive_unfolded. 2: apply eq_symmetric_unfolded; apply Lim_const. apply Lim_wd'. intro; simpl in |- *. unfold integral_seq, Even_Partition_Sum, Partition_Sum in |- *. eapply eq_transitive_unfolded. apply Mengolli_Sum with (f := fun (i : nat) (Hi : i <= S n) => Even_Partition Hab _ (O_S n) i Hi). red in |- *; intros. apply prf1; auto. intros; simpl in |- *; rational. apply cg_minus_wd; [ apply finish | apply start ]. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)