proposition: Theorem reflection_test3: forall (x y z t u : Z), (x * (((y * z) *1 )* (t * u)) = (x * (1 * y)) * (z * (t * u)) * 1)%Z.
proof: Proof. intros; assoc_eq Z Zmult 1%Z Zmult_assoc Zmult_1_l Zmult_1_r. Qed.
imports: ZArith List Arith Zwf Relations Inverse_Image Transitive_Closure Zdiv