proposition: Lemma one_div_succ_pos : forall i, ([0]:R) [<] one_div_succ i.
proof: Proof. intro. unfold one_div_succ in |- *. unfold Snring in |- *. apply recip_resp_pos. apply nring_pos. auto with arith. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)