proposition: Lemma compact_part_hyp : forall i Hi, compact a b Hab (compact_part i Hi).
proof: Proof. intros; unfold compact_part in |- *. split. astepl (a[+][0]); apply plus_resp_leEq_lft. astepl (ZeroR[*][0]); apply mult_resp_leEq_both; try apply leEq_reflexive. apply nring_nonneg. apply shift_leEq_div. apply pos_compact_nat. apply shift_leEq_minus; rstepl a; apply less_leEq; assumption. rstepr (a[+]nring compact_nat[*] (b[-]a[/] _[//]pos_ap_zero _ _ pos_compact_nat)). apply plus_resp_leEq_lft. apply mult_resp_leEq_rht; try apply nring_nonneg. apply nring_leEq; assumption. apply shift_leEq_div. apply pos_compact_nat. apply shift_leEq_minus; rstepl a; apply less_leEq; assumption. Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists