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