proposition: Lemma compact_less : forall i Hi HSi, [0] [<] compact_part (S i) HSi[-]compact_part i Hi.
proof: Proof. intros i H1 H2. apply shift_less_minus; astepl (compact_part _ H1). unfold compact_part in |- *. apply plus_resp_less_lft. apply mult_resp_less. simpl in |- *; apply less_plusOne. apply div_resp_pos. apply pos_compact_nat. apply shift_less_minus; astepl a; assumption. Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists