proposition: Lemma pos_compact_nat : [0] [<] nring (R:=IR) compact_nat.
proof: Proof. apply less_leEq_trans with (b[-]a[/] e[//]pos_ap_zero _ _ He). rstepr ((b[-]a) [*] ([1][/] e[//]pos_ap_zero _ _ He)). apply mult_resp_pos. apply shift_less_minus; astepl a; assumption. apply recip_resp_pos; assumption. unfold compact_nat in |- *; apply proj2_sigT. Qed.
imports: CoRN.algebra.CSetoidInc CoRN.reals.RealLists