proposition: Lemma Qmult_strext0 : forall x1 x2 y1 y2 : Q, (x1*y1/=x2*y2) -> (x1/=x2) or (y1/=y2).
proof: Proof. intros x1 x2 y1 y2 X. case (Qeq_dec x1 x2). right. intros ?. apply X. apply Qmult_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