proposition: Lemma one_div_succ_resp_less : forall i j, i < j -> one_div_succ j [<] one_div_succ (R:=R) i.
proof: Proof. intros. unfold one_div_succ in |- *. unfold Snring in |- *. intros. apply recip_resp_less. apply pos_nring_S. apply nring_less. auto with arith. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)