proposition: Lemma monotonous_integral : (forall x, I x -> forall Hx Hx', F x Hx [<=] G x Hx') -> Integral F contF [<=] Integral G contG.
proof: Proof. intros. unfold integral in |- *. apply Lim_leEq_Lim. intro n; simpl in |- *. unfold integral_seq, Even_Partition_Sum, Partition_Sum in |- *. apply Sumx_resp_leEq; intros i Hi. apply mult_resp_leEq_rht. apply H. Opaque nring. unfold I, Partition_imp_points in |- *; simpl in |- *. apply compact_partition_lemma; auto with arith. apply leEq_transitive with (AntiMesh (Even_Partition Hab (S n) (O_S n))). apply AntiMesh_nonneg. apply AntiMesh_lemma. Qed.
imports: CoRN.ftc.RefLemma Coq(Lia)