proposition: Lemma nring_Q : forall n : nat, nring (R:=Q_as_CRing) n[=]inject_Z n.
proof: Proof. intro n. induction n as [| n Hrecn]. change (Qmake 0%Z 1%positive==Qmake 0%Z 1%positive) in |- *. change ([0][=]([0]:Q_as_CRing)) in |- *. apply eq_reflexive_unfolded. change (nring (R:=Q_as_CRing) n[+][1][=]inject_Z (S n)) in |- *. Step_final ((inject_Z n:Q_as_CRing)[+][1]). astepl ((inject_Z n:Q_as_CRing)[+]inject_Z 1). simpl in |- *. red in |- *. unfold Qplus in |- *. simpl in |- *. rewrite Zpos_mult_morphism in |- *. rewrite succ_nat in |- *. ring. Qed.
imports: CoRN.model.abgroups.Qabgroup CoRN.algebra.CRings CoRN.model.rings.Zring