proposition: Lemma Zmult_absorb : forall x y z : Z, x <> 0%Z -> (x * y)%Z = (x * z)%Z -> y = z.
proof: Proof. intros x y z H H0. case (dec_eq y z). intro H1. assumption. intro H1. case (not_Zeq y z). assumption. intro H2. case (not_Zeq x 0). assumption. intro H3. exfalso. cut (x * y > x * z)%Z. intro H4. cut ((x * y)%Z <> (x * z)%Z). intro H5. apply H5. assumption. exact (Zgt_not_eq (x * y) (x * z) H4). exact (Zlt_conv_mult_l x y z H3 H2). intro H3. exfalso. cut (x * y < x * z)%Z. intro H4. cut ((x * y)%Z <> (x * z)%Z). intro H5. apply H5. assumption. exact (Zorder.Zlt_not_eq (x * y) (x * z) H4). apply Zlt_reg_mult_l. exact (Z.lt_gt 0 x H3). assumption. intro H2. apply False_ind. cut (x * z < x * y)%Z. intro H3. cut ((x * z)%Z <> (x * y)%Z). intro H4. apply H4. apply (sym_eq (A:=Z)). assumption. exact (Zorder.Zlt_not_eq (x * z) (x * y) H3). apply False_ind. case (not_Zeq x 0). assumption. intro H3. cut (x * z > x * y)%Z. intro H4. cut ((x * z)%Z <> (x * y)%Z). intro H5. apply H5. apply (sym_eq (A:=Z)). assumption. exact (Zgt_not_eq (x * z) (x * y) H4). exact (Zlt_conv_mult_l x z y H3 H2). intro H3. cut (x * z < x * y)%Z. intro H4. cut ((x * z)%Z <> (x * y)%Z). intro H5. apply H5. apply (sym_eq (A:=Z)). assumption. exact (Zorder.Zlt_not_eq (x * z) (x * y) H4). apply Zlt_reg_mult_l. exact (Z.lt_gt 0 x H3). auto. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid