proposition: Lemma ing_n : forall x n H1 H2, (inject_Q x[/] nring n[//]H2) [=] inject_Q (x[/] nring n[//]H1).
proof: Proof. intros. apply mult_cancel_lft with (inject_Q (nring (R:=F) n)). apply Greater_imp_ap. astepr (nring (R:=R_COrdField') n). apply nring_pos. apply Nat.neq_0_lt_0. apply Nat.neq_sym. apply nring_ap_zero_imp with F. assumption. apply ing_nring. apply eq_transitive_unfolded with (inject_Q x). rstepr (nring n[*] (inject_Q x[/] nring n[//]H2)). apply mult_wdl. apply eq_symmetric_unfolded. apply ing_nring. apply eq_symmetric_unfolded. apply eq_transitive_unfolded with (inject_Q (nring n[*] (x[/] nring n[//]H1))). apply eq_symmetric_unfolded. apply ing_mult. apply ing_eq. rational. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals