proposition: Lemma injZ_eq : forall x y : Z, x = y -> (inject_Z x:Q_as_CRing)[=]inject_Z y.
proof: Proof. intros. unfold inject_Z in |- *. simpl in |- *. red in |- *. simpl in |- *. rewrite H; trivial. Qed.
imports: CoRN.model.abgroups.Qabgroup CoRN.algebra.CRings CoRN.model.rings.Zring