proposition: Lemma Zmult_strext0 : forall x1 x2 y1 y2 : Z, (x1 * y1{#Z}x2 * y2) -> (x1{#Z}x2) or (y1{#Z}y2).
proof: Proof. unfold ap_Z in |- *. intros x1 x2 y1 y2 H. case (Z.eq_dec x1 x2). intro e. right. red in |- *. intro H0. apply H. exact (f_equal2 Zmult e H0). auto. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq.Setoids.Setoid