proposition: Theorem Zsgn_5 : forall a b x y : Z, x <> 0%Z -> y <> 0%Z -> (Z.sgn a * x)%Z = (Z.sgn b * y)%Z -> (Z.sgn a * y)%Z = (Z.sgn b * x)%Z.
proof: Proof. intros a b x y H H0. case a. case b. simpl in |- *. trivial. intro p. unfold Z.sgn in |- *. intro H1. rewrite Zmult_1_l in H1. simpl in H1. elim H0. auto. intro p. unfold Z.sgn in |- *. intro H1. elim H0. apply Z.opp_inj. simpl in |- *. transitivity (-1 * y)%Z; auto. intro p. unfold Z.sgn at 1 in |- *. unfold Z.sgn at 2 in |- *. intro H1. transitivity y. rewrite Zmult_1_l. reflexivity. transitivity (Z.sgn b * (Z.sgn b * y))%Z. case (Zsgn_1 b). intro H2. case H2. intro H3. elim H. rewrite H3 in H1. change ((1 * x)%Z = 0%Z) in H1. rewrite Zmult_1_l in H1. assumption. intro H3. rewrite H3. rewrite Zmult_1_l. rewrite Zmult_1_l. reflexivity. intro H2. rewrite H2. ring. rewrite Zmult_1_l in H1. rewrite H1. reflexivity. intro p. unfold Z.sgn at 1 in |- *. unfold Z.sgn at 2 in |- *. intro H1. transitivity (Z.sgn b * (-1 * (Z.sgn b * y)))%Z. case (Zsgn_1 b). intro H2. case H2. intro H3. elim H. apply Z.opp_inj. transitivity (-1 * x)%Z. ring. unfold Z.opp in |- *. rewrite H3 in H1. transitivity (0 * y)%Z; auto. intro H3. rewrite H3. ring. intro H2. rewrite H2. ring. rewrite <- H1. ring. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)