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. unfold Z.sgn in |- *. intro. rewrite Zmult_1_l in H1. simpl in H1. apply False_ind. apply H0. symmetry in |- *. assumption. intro. unfold Z.sgn in |- *. intro. apply False_ind. apply H0. apply Z.opp_inj. simpl in |- *. transitivity (-1 * y)%Z. constructor. transitivity (0 * x)%Z. symmetry in |- *. assumption. simpl in |- *. reflexivity. intro. unfold Z.sgn at 1 in |- *. unfold Z.sgn at 2 in |- *. intro. transitivity y. rewrite Zmult_1_l. reflexivity. transitivity (Z.sgn b * (Z.sgn b * y))%Z. case (Zsgn_1' b). intro. case s. intro. apply False_ind. apply H. rewrite e in H1. change ((1 * x)%Z = 0%Z) in H1. rewrite Zmult_1_l in H1. assumption. intro. rewrite e. rewrite Zmult_1_l. rewrite Zmult_1_l. reflexivity. intro. rewrite e. ring. rewrite Zmult_1_l in H1. rewrite H1. reflexivity. intro. unfold Z.sgn at 1 in |- *. unfold Z.sgn at 2 in |- *. intro. transitivity (Z.sgn b * (-1 * (Z.sgn b * y)))%Z. case (Zsgn_1' b). intros. case s. intro. apply False_ind. apply H. apply Z.opp_inj. transitivity (-1 * x)%Z. ring. unfold Z.opp in |- *. rewrite e in H1. transitivity (0 * y)%Z. assumption. simpl in |- *. reflexivity. intro. rewrite e. ring. intro. rewrite e. ring. rewrite <- H1. ring. Qed.
imports: Coq(Lia)