proposition: Theorem reflection_test4 : forall x y z:Z, (x+(y+z) = (z+x)+y)%Z.
proof: Proof. intros x y z. comm_eq' Z Zplus Zplus_assoc Zplus_comm. Qed.
imports: ZArith List Arith Lia Zwf Relations Inverse_Image Transitive_Closure Zdiv