proposition: Lemma Qplus_strext0 : forall x1 x2 y1 y2 : Q, (x1+y1/=x2+y2) -> (x1/=x2) or (y1/=y2).
proof: Proof. unfold Qap in |- *. intros x1 x2 y1 y2 X. case (Qeq_dec x1 x2). intro e. right. red in |- *. intro H0. apply X. apply Qplus_comp; auto. tauto. Qed.
imports: CoRN.logic.CLogic Coq.Arith.Arith Coq.Arith.Peano_dec CoRN.model.structures.Zsec Coq.QArith.QArith CoRN.stdlib_omissions.Q