proposition: Lemma compact_partition_lemma : forall n Hn i, i <= n -> Compact Hab (a[+]nring i[*] (b[-]a[/] _[//]nring_ap_zero' _ n Hn)).
proof: Proof. intros n Hn i H; split. apply shift_leEq_plus'. astepl ZeroR. apply mult_resp_nonneg. apply nring_nonneg. apply shift_leEq_div. apply nring_pos; apply Nat.neq_0_lt_0; auto. apply shift_leEq_minus. rstepl a; assumption. apply shift_plus_leEq'. rstepr (nring n[*] (b[-]a[/] _[//]nring_ap_zero' _ _ Hn)). astepl ([0][+]nring i[*] (b[-]a[/] _[//]nring_ap_zero' _ _ Hn)). apply shift_plus_leEq. rstepr ((nring n[-]nring i) [*] (b[-]a[/] _[//]nring_ap_zero' _ _ Hn)). apply mult_resp_nonneg. apply shift_leEq_minus. astepl (nring (R:=IR) i). apply nring_leEq; assumption. apply shift_leEq_div. apply nring_pos; apply Nat.neq_0_lt_0; auto. apply shift_leEq_minus. rstepl a; assumption. Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists