proposition: Lemma injz_plus : forall m n : Z, (inject_Z (m + n):Q)==(inject_Z m:Q)+inject_Z n.
proof: Proof. intros m n. unfold inject_Z in |- *. simpl in |- *. unfold Qeq in |- *. unfold Qnum at 1 in |- *. unfold Qden at 2 in |- *. replace ((m + n) * 1)%Z with (m + n)%Z. replace (Qnum (Qmake m 1+Qmake n 1)%Q * 1)%Z with (Qnum (Qmake m 1+Qmake n 1)). unfold Qplus in |- *. simpl in |- *. ring. ring. ring. Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q