proposition: Lemma tech8 : forall n i:nat, (n <= S n + i)%nat.
proof: Proof. intros; induction i as [| i Hreci]. - replace (S n + 0)%nat with (S n); [ apply Nat.le_succ_diag_r | ring ]. - replace (S n + S i)%nat with (S (S n + i)). + apply le_S; assumption. + apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; do 2 rewrite S_INR; ring. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun ArithRing