proposition: Theorem Zeq_mult_simpl : forall a b c : Z, c <> 0%Z -> (a * c)%Z = (b * c)%Z -> a = b.
proof: Proof. intros a b c H H0. case (Zle_or_lt c 0); intros Zl1. apply Zle_antisym; apply Zmult_le_reg_r with (p := (- c)%Z); try apply Z.lt_gt; auto with zarith; repeat rewrite <- Zopp_mult_distr_r; rewrite H0; auto with zarith. apply Zle_antisym; apply Zmult_le_reg_r with (p := c); try apply Z.lt_gt; auto with zarith; rewrite H0; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz