proposition: Lemma one_div_succ_resp_leEq : forall m n, m <= n -> one_div_succ (R:=R) n [<=] one_div_succ m.
proof: Proof. unfold one_div_succ in |- *. unfold Snring in |- *. intros. apply recip_resp_leEq. apply pos_nring_S. apply nring_leEq. auto with arith. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)