proposition: Lemma compact_leEq : forall i Hi HSi, compact_part (S i) HSi[-]compact_part i Hi [<=] e.
proof: Proof. intros i H1 H2. unfold compact_part in |- *; simpl in |- *. rstepl (b[-]a[/] _[//]pos_ap_zero _ _ pos_compact_nat). apply shift_div_leEq. apply pos_compact_nat. apply shift_leEq_mult' with (pos_ap_zero _ _ He). assumption. exact (ProjT2 (Archimedes _)). Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists