proposition: Lemma Zmult_absorb : forall x y z : Z, x <> 0%Z -> (x * y)%Z = (x * z)%Z -> y = z.
proof: Proof. intros. case (dec_eq y z). intro. assumption. intro. case (not_Zeq y z). assumption. intro. case (not_Zeq x 0). assumption. intro. apply False_ind. cut (x * y > x * z)%Z. intro. cut ((x * y)%Z <> (x * z)%Z). intro. apply H5. assumption. exact (Zgt_not_eq (x * y) (x * z) H4). exact (Zlt_conv_mult_l x y z H3 H2). intro. apply False_ind. cut (x * y < x * z)%Z. intro. cut ((x * y)%Z <> (x * z)%Z). intro. apply H5. assumption. exact (Zorder.Zlt_not_eq (x * y) (x * z) H4). cut (x > 0)%Z. intro. exact (Zlt_reg_mult_l x y z H4 H2). exact (Z.lt_gt 0 x H3). intro. apply False_ind. cut (x * z < x * y)%Z. intro. cut ((x * z)%Z <> (x * y)%Z). intro. 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. cut (x * z > x * y)%Z. intro. cut ((x * z)%Z <> (x * y)%Z). intro. 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. cut (x * z < x * y)%Z. intro. cut ((x * z)%Z <> (x * y)%Z). intro. apply H5. apply (sym_eq (A:=Z)). assumption. exact (Zorder.Zlt_not_eq (x * z) (x * y) H4). cut (x > 0)%Z. intro. exact (Zlt_reg_mult_l x z y H4 H2). exact (Z.lt_gt 0 x H3). Qed.
imports: Coq(Lia)