proposition: Lemma injz_Nring : forall n, nring (R:=Q_as_CRing) n[=]inject_Z (nring (R:=Z_as_CRing) n).
proof: Proof. intro n. induction n as [| n Hrecn]. change (([0]:Q_as_CRing)[=][0]) in |- *. apply eq_reflexive_unfolded. change (nring (R:=Q_as_CRing) n[+][1][=]inject_Z (nring (R:=Z_as_CRing) n[+][1])) in |- *. Step_final ((inject_Z (nring (R:=Z_as_CRing) n):Q_as_CRing)[+][1]). astepl ((inject_Z (nring (R:=Z_as_CRing) n):Q_as_CRing)[+] inject_Z ([1]:Z_as_CRing)). apply eq_symmetric_unfolded. apply injz_plus. Qed.
imports: CoRN.model.abgroups.Qabgroup CoRN.algebra.CRings CoRN.model.rings.Zring